complementedLattice_Ici — Mathlib

English

From a ≤ b there exists a' with a ⊓ a' = a and a ∨ a' = b, i.e., a decomposition via a disjoint piece.

Русский

Из a ≤ b следует существование a' с a ⊓ a' = a и a ∨ a' = b; это разложение через несовпадающую часть.

LaTeX

$$$\exists a':\; (a\wedge a')=a \land (a\vee a')=b$$$

Lean4

instance complementedLattice_Ici : ComplementedLattice (Set.Ici a) where
  exists_isCompl := fun ⟨x, hx⟩ => by
    simp_rw [Set.Ici.isCompl_iff]
    obtain ⟨y, rfl, hcodisjoint⟩ := exists_inf_eq_and_codisjoint hx
    exact ⟨⟨y, inf_le_right⟩, rfl, hcodisjoint⟩

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