locallyFinite_comp_iff — Mathlib

English

A set of equivalent conditions for locally finite sum splitting.

Русский

Эквивалентные условия локально конечной суммы через разбиение.

LaTeX

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

Lean4

@[simp]
theorem locallyFinite_comp_iff (e : ι' ≃ ι) : LocallyFinite (f ∘ e) ↔ LocallyFinite f :=
  ⟨fun h => by simpa only [comp_def, e.apply_symm_apply] using h.comp_injective e.symm.injective, fun h =>
    h.comp_injective e.injective⟩

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