locallyFinite_sum — Mathlib

English

The equivalence for locally finite functions on a sum type holds.

Русский

Эквивалентность локально конечной функции на суммарном типе сохраняется.

LaTeX

$$LocallyFinite f ↔ (LocallyFinite (Function.comp f Sum.inl) ∧ LocallyFinite (Function.comp f Sum.inr))$$

Lean4

theorem locallyFinite_sum {f : ι ⊕ ι' → Set X} :
    LocallyFinite f ↔ LocallyFinite (f ∘ Sum.inl) ∧ LocallyFinite (f ∘ Sum.inr) := by
  simp only [locallyFinite_iff_smallSets, ← forall_and, ← finite_preimage_inl_and_inr, preimage_setOf_eq, (· ∘ ·),
    eventually_and]

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