finite_biUnion'' — Mathlib

English

Example: If p is a predicate over an index i and t i are finite for i satisfying p, then ⋃ x ∈ {i | p i}, t x is finite.

Русский

Пример: если p — предикат над индексом i, и t i конечно при i, удовлетворяющем p, то ⋃ i ∈ {i | p i} t i конечно.

LaTeX

$$$\\operatorname{Finite}\\left(\\bigcup_{i \\in \\{\,i \\mid p(i)\,\\}} t(i)\\right)$$$

Lean4

/-- Example: `Finite (⋃ (i < n), f i)` where `f : ℕ → Set α` and `[∀ i, Finite (f i)]`
(when given instances from `Order.Interval.Finset.Nat`).
-/
instance finite_biUnion'' {ι : Type*} (p : ι → Prop) [h : Finite {x | p x}] (t : ι → Set α) [∀ i, Finite (t i)] :
    Finite (⋃ (x) (_ : p x), t x) :=
  @Finite.Set.finite_biUnion' _ _ (setOf p) h t _

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