finite_image_fst_and_snd_iff — Mathlib

English

For any set s of α × β, the finiteness of the images under fst and snd is equivalent to the finiteness of s itself.

Русский

Для множества s ⊆ α × β конечность образов fst(s) и snd(s) эквивалентна конечности самого s.

LaTeX

$$$ (\mathrm{image} \mathrm{fst} \ s).Finite \land (\mathrm{image} \mathrm{snd} \ s).Finite \iff s.Finite $$$

Lean4

theorem finite_image_fst_and_snd_iff {s : Set (α × β)} : (Prod.fst '' s).Finite ∧ (Prod.snd '' s).Finite ↔ s.Finite :=
  ⟨fun h => (h.1.prod h.2).subset fun _ h => ⟨mem_image_of_mem _ h, mem_image_of_mem _ h⟩, fun h =>
    ⟨h.image _, h.image _⟩⟩

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