complementedLattice_Iic — Mathlib

English

The interval Iic a is complemented; any element admits a complement within Iic a.

Русский

Интервал Iic a комплементирован; любой элемент имеет внутри Iic a комплемент.

LaTeX

$$$\text{ComplementedLattice }(\mathrm{Set.Iic}\ a)$$$

Lean4

instance complementedLattice_Iic : ComplementedLattice (Set.Iic a) where
  exists_isCompl := fun ⟨x, hx⟩ => by
    simp_rw [Set.Iic.isCompl_iff]
    obtain ⟨y, hdisjoint, rfl⟩ := exists_disjoint_and_sup_eq hx
    exact ⟨⟨y, le_sup_right⟩, hdisjoint, rfl⟩

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