finsetSup' — Mathlib

English

A variant of FinsetSup for nonempty Finset s: if each t(i) is retrocompact, then s.sup' hs t is retrocompact.

Русский

Вариант FinsetSup' для непустого Finset s: если каждый t(i) ретрокомпактен, то s.sup' hs t ретрокомпактен.

LaTeX

$$$\text{IsRetrocompact}(s.\sup' hs\ t)$$$

Lean4

theorem finsetSup' {ι : Type*} {s : Finset ι} {hs} {t : ι → Set X} (ht : ∀ i ∈ s, IsRetrocompact (t i)) :
    IsRetrocompact (s.sup' hs t) := by rw [Finset.sup'_eq_sup]; exact .finsetSup ht

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