infClosed_pi — Mathlib

English

If each f i is inf-closed, then the pi-type s.pi t is inf-closed.

Русский

Если каждый f(i) инф-замкнут, то π-образование замкнуто.

LaTeX

$$$ (\\forall i, \\text{InfClosed}(t(i))) \\rightarrow \\text{InfClosed}(\\{f: i \\mapsto t(i)\\}) $$$

Lean4

theorem infClosed_pi {ι : Type*} {α : ι → Type*} [∀ i, SemilatticeInf (α i)] {s : Set ι} {t : ∀ i, Set (α i)}
    (ht : ∀ i ∈ s, InfClosed (t i)) : InfClosed (s.pi t) := fun _a ha _b hb _i hi ↦ ht _ hi (ha _ hi) (hb _ hi)

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