finite_image2 — Mathlib

English

The image2 set is finite iff s and t are finite or at least one of s, t is empty, under suitable injectivity conditions.

Русский

Образ image2 фермы относительно s и t конечен тогда и только тогда, когда либо s и t конечны, либо один из них пуст.

LaTeX

$$$ (image2 f s t).Finite \iff (s.Finite \land t.Finite) \lor s = \emptyset \lor t = \emptyset $$$

Lean4

theorem finite_image2 (hfs : ∀ b ∈ t, InjOn (f · b) s) (hft : ∀ a ∈ s, InjOn (f a) t) :
    (image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅ :=
  by
  rw [← not_infinite, infinite_image2 hfs hft]
  simp [not_or, -not_and, not_and_or, not_nonempty_iff_eq_empty]
  aesop

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