infClosure_supClosure — Mathlib

English

InfClosure of SupClosure s equals latticeClosure s.

Русский

InfClosure(SupClosure(s)) = latticeClosure(s).

LaTeX

$$$\infClosure(\supClosure s) = \mathrm{latticeClosure} s$$$

Lean4

@[simp]
theorem infClosure_supClosure (s : Set α) : infClosure (supClosure s) = latticeClosure s :=
  le_antisymm
      (infClosure_min (supClosure_min subset_latticeClosure isSublattice_latticeClosure.1)
        isSublattice_latticeClosure.2) <|
    latticeClosure_min (subset_supClosure.trans subset_infClosure)
      ⟨supClosed_supClosure.infClosure, infClosed_infClosure⟩

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