finite_preimage_inl_and_inr — Mathlib

English

For s ⊆ α ⊕ β, the left and right preimages are finite if and only if s is finite.

Русский

Для множества s ⊆ (α ⊕ β) праобраз слева и справа конечны тогда и только тогда, когда s конечно.

LaTeX

$$$(\mathrm{preimage}(\mathrm{Sum.inl}, s) \text{ finite}) \land (\mathrm{preimage}(\mathrm{Sum.inr}, s) \text{ finite}) \\iff s \text{ finite}$$$

Lean4

theorem finite_preimage_inl_and_inr {s : Set (α ⊕ β)} : (Sum.inl ⁻¹' s).Finite ∧ (Sum.inr ⁻¹' s).Finite ↔ s.Finite :=
  ⟨fun h => image_preimage_inl_union_image_preimage_inr s ▸ (h.1.image _).union (h.2.image _), fun h =>
    ⟨h.preimage Sum.inl_injective.injOn, h.preimage Sum.inr_injective.injOn⟩⟩

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