English
Let α be a modular lattice that is compactly generated. If for a family {f(i)} indexed over a set s every interval Iic(f(i)) is a complemented lattice and the supremum of the family equals top, then α is a complemented lattice.
Русский
Пусть α — модульная решетка, которая компактно порождается. Если для семейства {f(i)} индексированного по множеству s каждый интервал Iic(f(i)) комплементирован, и верхняя граница объединения этих f(i) достигает ⊤, то α является комплементированной решеткой.
LaTeX
$$$IsModularLattice(\alpha) \wedge IsCompactlyGenerated(\alpha) \wedge \left( \forall i \in s,\; ComplementedLattice(Iic(f(i))) \right) \wedge \bigvee_{i \in s} f(i) = \top \Rightarrow ComplementedLattice(\alpha).$$$
Lean4
theorem complementedLattice_of_complementedLattice_Iic [IsModularLattice α] [IsCompactlyGenerated α] {s : Set ι}
{f : ι → α} (h : ∀ i ∈ s, ComplementedLattice <| Iic (f i)) (h' : ⨆ i ∈ s, f i = ⊤) : ComplementedLattice α :=
by
apply complementedLattice_of_sSup_atoms_eq_top
have : ∀ i ∈ s, ∃ t : Set α, f i = sSup t ∧ ∀ a ∈ t, IsAtom a := fun i hi ↦
by
replace h := complementedLattice_iff_isAtomistic.mp (h i hi)
obtain ⟨u, hu, hu'⟩ := eq_sSup_atoms (⊤ : Iic (f i))
refine ⟨(↑) '' u, ?_, ?_⟩
· replace hu : f i = ↑(sSup u) := Subtype.ext_iff.mp hu
simp_rw [hu, Iic.coe_sSup]
· rintro b ⟨⟨a, ha'⟩, ha, rfl⟩
exact IsAtom.of_isAtom_coe_Iic (hu' _ ha)
choose t ht ht' using this
let u : Set α := ⋃ i, ⋃ hi : i ∈ s, t i hi
have hu₁ : u ⊆ {a | IsAtom a} :=
by
rintro a ⟨-, ⟨i, rfl⟩, ⟨-, ⟨hi, rfl⟩, ha : a ∈ t i hi⟩⟩
exact ht' i hi a ha
have hu₂ : sSup u = ⨆ i ∈ s, f i := by simp_rw [u, sSup_iUnion, biSup_congr' ht]
rw [eq_top_iff, ← h', ← hu₂]
exact sSup_le_sSup hu₁
