supClosure_infClosure — Mathlib

English

SupClosure of infClosure s equals latticeClosure s.

Русский

SupClosure infClosure(s) равно latticeClosure(s).

LaTeX

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

Lean4

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

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