English
Let α(i) be a family of semilattices, s ⊆ ι, and t(i) ⊆ α(i) be sup-closed for all i ∈ s. Then the dependent product s → t is sup-closed.
Русский
Пусть α(i) — семейство полуправд, s ⊆ ι, и t(i) ⊆ α(i) замкнуты по ⊔ для всех i ∈ s. Тогда зависимое произведение s → t замкнуто по ⊔.
LaTeX
$$$ (\\forall i \\in s)\\, \\operatorname{InfClosed}(t(i)) \\Rightarrow \\operatorname{InfClosed}(s \\to t) $$$
Lean4
theorem supClosed_pi {ι : Type*} {α : ι → Type*} [∀ i, SemilatticeSup (α i)] {s : Set ι} {t : ∀ i, Set (α i)}
(ht : ∀ i ∈ s, SupClosed (t i)) : SupClosed (s.pi t) := fun _a ha _b hb _i hi ↦ ht _ hi (ha _ hi) (hb _ hi)
