finsetInf' — Mathlib

English

The finitary infimum of locally constructible sets is locally constructible.

Русский

Нижняя граница в рамках конечного множества конструируемых множеств локально конструируема.

LaTeX

$$$IsLocallyConstructible(s.inf' t)$.$$

Lean4

theorem finsetInf' {ι : Type*} {s : Finset ι} {hs} {t : ι → Set X} (ht : ∀ i ∈ s, IsLocallyConstructible (t i)) :
    IsLocallyConstructible (s.inf' hs t) := by rw [Finset.inf'_eq_inf]; exact .finsetInf ht

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