Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(order/complete_lattice): independence of an indexed family #7199

Closed
wants to merge 14 commits into from
22 changes: 11 additions & 11 deletions src/order/compactly_generated.lean
Original file line number Diff line number Diff line change
Expand Up @@ -300,9 +300,9 @@ le_antisymm (begin
exact (le_inf hcinf.1 ht2).trans (le_bsupr t ht1),
end) (supr_le $ λ t, supr_le $ λ h, inf_le_inf_left _ ((finset.sup_eq_Sup t).symm ▸ (Sup_le_Sup h)))

theorem complete_lattice.independent_iff_finite {s : set α} :
complete_lattice.independent s ↔
∀ t : finset α, ↑t ⊆ s → complete_lattice.independent (↑t : set α) :=
theorem complete_lattice.sindependent_iff_finite {s : set α} :
complete_lattice.sindependent s ↔
∀ t : finset α, ↑t ⊆ s → complete_lattice.sindependent (↑t : set α) :=
⟨λ hs t ht, hs.mono ht, λ h a ha, begin
rw [disjoint_iff, inf_Sup_eq_supr_inf_sup_finset, supr_eq_bot],
intro t,
Expand All @@ -316,14 +316,14 @@ theorem complete_lattice.independent_iff_finite {s : set α} :
exact ⟨ha, set.subset.trans ht (set.diff_subset _ _)⟩ }
end⟩

lemma complete_lattice.independent_Union_of_directed {η : Type*}
lemma complete_lattice.sindependent_Union_of_directed {η : Type*}
{s : η → set α} (hs : directed (⊆) s)
(h : ∀ i, complete_lattice.independent (s i)) :
complete_lattice.independent (⋃ i, s i) :=
(h : ∀ i, complete_lattice.sindependent (s i)) :
complete_lattice.sindependent (⋃ i, s i) :=
begin
by_cases hη : nonempty η,
{ resetI,
rw complete_lattice.independent_iff_finite,
rw complete_lattice.sindependent_iff_finite,
intros t ht,
obtain ⟨I, fi, hI⟩ := set.finite_subset_Union t.finite_to_set ht,
obtain ⟨i, hi⟩ := hs.finset_le fi.to_finset,
Expand All @@ -335,10 +335,10 @@ end

lemma complete_lattice.independent_sUnion_of_directed {s : set (set α)}
(hs : directed_on (⊆) s)
(h : ∀ a ∈ s, complete_lattice.independent a) :
complete_lattice.independent (⋃₀ s) :=
(h : ∀ a ∈ s, complete_lattice.sindependent a) :
complete_lattice.sindependent (⋃₀ s) :=
by rw set.sUnion_eq_Union; exact
complete_lattice.independent_Union_of_directed hs.directed_coe (by simpa using h)
complete_lattice.sindependent_Union_of_directed hs.directed_coe (by simpa using h)


end
Expand Down Expand Up @@ -422,7 +422,7 @@ end, λ _, and.left⟩⟩
theorem is_complemented_of_Sup_atoms_eq_top (h : Sup {a : α | is_atom a} = ⊤) : is_complemented α :=
⟨λ b, begin
obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ := zorn.zorn_subset
{s : set α | complete_lattice.independent s ∧ b ⊓ Sup s = ⊥ ∧ ∀ a ∈ s, is_atom a} _,
{s : set α | complete_lattice.sindependent s ∧ b ⊓ Sup s = ⊥ ∧ ∀ a ∈ s, is_atom a} _,
{ refine ⟨Sup s, le_of_eq b_inf_Sup_s, _⟩,
rw [← h, Sup_le_iff],
intros a ha,
Expand Down
43 changes: 36 additions & 7 deletions src/order/complete_lattice.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1144,32 +1144,61 @@ variables [complete_lattice α]

/-- An independent set of elements in a complete lattice is one in which every element is disjoint
from the `Sup` of the rest. -/
def independent (s : set α) : Prop := ∀ ⦃a⦄, a ∈ s → disjoint a (Sup (s \ {a}))
def sindependent (s : set α) : Prop := ∀ ⦃a⦄, a ∈ s → disjoint a (Sup (s \ {a}))
kbuzzard marked this conversation as resolved.
Show resolved Hide resolved

variables {s : set α} (hs : independent s)
variables {s : set α} (hs : sindependent s)

@[simp]
lemma independent_empty : independent (∅ : set α) :=
lemma sindependent_empty : sindependent (∅ : set α) :=
λ x hx, (set.not_mem_empty x hx).elim

theorem independent.mono {t : set α} (hst : t ⊆ s) :
independent t :=
theorem sindependent.mono {t : set α} (hst : t ⊆ s) :
sindependent t :=
λ a ha, (hs (hst ha)).mono_right (Sup_le_Sup (diff_subset_diff_left hst))

/-- If the elements of a set are independent, then any pair within that set is disjoint. -/
lemma independent.disjoint {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : x ≠ y) : disjoint x y :=
lemma sindependent.disjoint {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : x ≠ y) : disjoint x y :=
disjoint_Sup_right (hs hx) ((mem_diff y).mpr ⟨hy, by simp [h.symm]⟩)

include hs

/-- If the elements of a set are independent, then any element is disjoint from the `Sup` of some
subset of the rest. -/
lemma independent.disjoint_Sup {x : α} {y : set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : x ∉ y) :
lemma sindependent.disjoint_Sup {x : α} {y : set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : x ∉ y) :
disjoint x (Sup y) :=
begin
have := (hs.mono $ insert_subset.mpr ⟨hx, hy⟩) (mem_insert x _),
rw [insert_diff_of_mem _ (mem_singleton _), diff_singleton_eq_self hxy] at this,
exact this,
end

omit hs

/-- An independent indexed family of elements in a complete lattice is one in which every element
is disjoint from the `Sup` of the rest. -/
kbuzzard marked this conversation as resolved.
Show resolved Hide resolved
kbuzzard marked this conversation as resolved.
Show resolved Hide resolved
def independent {ι : Sort*} {α : Type*} [complete_lattice α] (s : ι → α): Prop :=
kbuzzard marked this conversation as resolved.
Show resolved Hide resolved
∀ ⦃i : ι⦄, disjoint (s i) (⨆ (j ≠ i), s j)
kbuzzard marked this conversation as resolved.
Show resolved Hide resolved

lemma sindependent_iff {α : Type*} [complete_lattice α] (s : set α) :
sindependent s ↔ independent (coe : s → α) :=
begin
simp_rw [independent, sindependent, set_coe.forall, Sup_eq_supr],
apply forall_congr, intro a, apply forall_congr, intro ha,
congr' 2,
convert supr_subtype.symm,
simp [supr_and],
end

variables {t : ι → α} (ht : independent t)

@[simp]
lemma independent_empty (t : empty → α) : independent t.

@[simp]
lemma independent_pempty (t : pempty → α) : independent t.

/-- If the elements of a set are independent, then any pair within that set is disjoint. -/
lemma independent.disjoint {x y : ι} (h : x ≠ y) : disjoint (t x) (t y) :=
disjoint_Sup_right (@ht x) ⟨y, by simp [h.symm]⟩

kbuzzard marked this conversation as resolved.
Show resolved Hide resolved
end complete_lattice