sInf — Mathlib

English

If every member s in a family S is closed under f, then the infimum sInf S (the intersection of all members of S) is closed under f.

Русский

Если для каждого множества s из семейства S верно, что s замкнуто относительно f, тогда пересечение всех s в S замкнуто относительно f.

LaTeX

$$$$ (\forall S \in \mathcal{S}, ClosedUnder\ f\ S) \Rightarrow ClosedUnder\ f\ (\bigcap_{S \in \mathcal{S}} S). $$$$

Lean4

theorem sInf (hS : ∀ s, s ∈ S → ClosedUnder f s) : ClosedUnder f (sInf S) := fun x h s hs => hS s hs x fun i => h i s hs

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