English
In an atomic lattice, for given b ≤ c and c = sSup of atoms below c, there exists a set s of atoms with sSupIndep, Disjoint b (sSup s), and b ⊔ sSup s = c, with every element of s an atom.
Русский
В атомной решётке при b ≤ c и c = sSup атомов ниже c существует множество атомов s и т.д.
LaTeX
$$$ \exists s \subseteq \{a : α \mid IsAtom a \land a \le c\},\; sSupIndep s \land Disjoint b (sSup s) \land b \lor sSup s = c \land \forall a \in s, IsAtom a$$$
Lean4
/-- In an atomic lattice, every element `b` has a complement of the form `sSup s` relative to a
given element `c`, where each element of `s` is an atom.
See also `complementedLattice_of_sSup_atoms_eq_top`. -/
theorem exists_sSupIndep_disjoint_sSup_atoms (b c : α) (hbc : b ≤ c) (h : sSup ({a ≤ c | IsAtom a}) = c) :
∃ s : Set α, sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a⦄, a ∈ s → IsAtom a := by
-- porting note(https://github.com/leanprover-community/mathlib4/issues/5732):
-- `obtain` chokes on the placeholder.
have zorn :=
zorn_subset (S := {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c}) fun c hc1 hc2 =>
⟨⋃₀ c,
⟨iSupIndep_sUnion_of_directed hc2.directedOn fun s hs => (hc1 hs).1, ?_, fun a ⟨s, sc, as⟩ =>
(hc1 sc).2.2 a as⟩,
fun _ => Set.subset_sUnion_of_mem⟩
swap
· rw [sSup_sUnion, ← sSup_image, DirectedOn.disjoint_sSup_right]
· rintro _ ⟨s, hs, rfl⟩
exact (hc1 hs).2.1
· rw [directedOn_image]
exact hc2.directedOn.mono @fun s t => sSup_le_sSup
simp_rw [maximal_subset_iff] at zorn
obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ := zorn
refine ⟨s, s_ind, b_inf_Sup_s, le_antisymm ?_ ?_, fun a ha ↦ (s_atoms a ha).1⟩
· simp_all
rw [← h, sSup_le_iff]
intro a ha
rw [← inf_eq_left]
refine (ha.2.le_iff.mp inf_le_left).resolve_left fun con => ha.2.1 ?_
rw [← con, eq_comm, inf_eq_left]
refine (le_sSup ?_).trans le_sup_right
rw [← disjoint_iff] at con
have a_dis_Sup_s : Disjoint a (sSup s) := con.mono_right le_sup_right
rw [s_max ⟨fun x hx => ?_, ?_, fun x hx => ?_⟩ Set.subset_union_left]
· exact Set.mem_union_right _ (Set.mem_singleton _)
· rw [sSup_union, sSup_singleton]
exact b_inf_Sup_s.disjoint_sup_right_of_disjoint_sup_left con.symm
· rw [Set.mem_union, Set.mem_singleton_iff] at hx
obtain rfl | xa := eq_or_ne x a
· simp only [Set.mem_singleton, Set.insert_diff_of_mem, Set.union_singleton]
exact con.mono_right ((sSup_le_sSup Set.diff_subset).trans le_sup_right)
· have h : (s ∪ { a }) \ { x } = s \ { x } ∪ { a } :=
by
simp only [Set.union_singleton]
rw [Set.insert_diff_of_notMem]
rw [Set.mem_singleton_iff]
exact Ne.symm xa
rw [h, sSup_union, sSup_singleton]
apply (s_ind (hx.resolve_right xa)).disjoint_sup_right_of_disjoint_sup_left (a_dis_Sup_s.mono_right _).symm
rw [← sSup_insert, Set.insert_diff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]
· rw [Set.mem_union, Set.mem_singleton_iff] at hx
obtain hx | rfl := hx
· exact s_atoms x hx
· exact ha.symm
