infClosed_sInter — Mathlib

English

If a family of sets is inf-closed, their sInter is inf-closed.

Русский

Если множество $S$ содержит инф-замкнутые множества, то их пересечение инф-замкнуто.

LaTeX

$$$ (\\forall s \\in S, \\text{InfClosed } s) \\Rightarrow \\text{InfClosed}(\\bigcap S) $$$

Lean4

theorem infClosed_sInter (hS : ∀ s ∈ S, InfClosed s) : InfClosed (⋂₀ S) := fun _a ha _b hb _s hs ↦
  hS _ hs (ha _ hs) (hb _ hs)

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