sumElim — Mathlib

English

Combining locally finite families on a sum type yields a locally finite combined family.

Русский

Сочетание локально конечных семейств на суммарном типе образует локально конечное объединение.

LaTeX

$$LocallyFinite f → LocallyFinite g → LocallyFinite (Sum.elim f g)$$

Lean4

theorem sumElim {g : ι' → Set X} (hf : LocallyFinite f) (hg : LocallyFinite g) : LocallyFinite (Sum.elim f g) :=
  locallyFinite_sum.mpr ⟨hf, hg⟩

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