isAtomistic_of_complementedLattice

English

For a directed family f, Disjoint (iSup f) a iff ∀ i, Disjoint (f i) a.

Русский

Для направленного семейства f: Disjoint (iSup f) a ⇔ ∀ i, Disjoint (f i) a.

LaTeX

$$$ \mathrm{Disjoint}\left(\big\vee_i f(i), a\right) \iff \forall i, \mathrm{Disjoint}(f(i), a) $$$

Lean4

/-- See [Lemma 5.1][calugareanu]. -/
instance (priority := 100) isAtomistic_of_complementedLattice [ComplementedLattice α] : IsAtomistic α :=
  CompleteLattice.isAtomistic_iff.2 fun b =>
    ⟨{a | IsAtom a ∧ a ≤ b}, by
      symm
      have hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b := sSup_le fun _ => And.right
      apply (lt_or_eq_of_le hle).resolve_left _
      intro con
      obtain ⟨c, hc⟩ := exists_isCompl (⟨sSup {a : α | IsAtom a ∧ a ≤ b}, hle⟩ : Set.Iic b)
      obtain rfl | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le c
      · exact ne_of_lt con (Subtype.ext_iff.1 (eq_top_of_isCompl_bot hc))
      · apply ha.1
        rw [eq_bot_iff]
        apply le_trans (le_inf _ hac) hc.disjoint.le_bot
        rw [← Subtype.coe_le_coe, Subtype.coe_mk]
        exact le_sSup ⟨ha.of_isAtom_coe_Iic, a.2⟩, fun _ => And.left⟩

Похожие утверждения