sInf_isClosed — Mathlib

English

If every element of S is closed, then sInf S is closed.

Русский

Если каждый элемент множества S замкнут, то infimum S замкнут.

LaTeX

$$$\\\\forall {\\\\alpha : Type*} [CompleteLattice {\\\\alpha}] {c : ClosureOperator {\\\\alpha}} {S : Set {\\\\alpha}}, (\\\\forall x \\in S, c.IsClosed x) \\\\Rightarrow c.IsClosed (sInf S)$$$

Lean4

theorem sInf_isClosed {c : ClosureOperator α} {S : Set α} (H : ∀ x ∈ S, c.IsClosed x) : c.IsClosed (sInf S) :=
  isClosed_iff_closure_le.mpr <|
    le_of_le_of_eq c.monotone.map_sInf_le <| Eq.trans (biInf_congr (c.isClosed_iff.mp <| H · ·)) sInf_eq_iInf.symm

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