pairwise_image — Mathlib

English

If f is injective on s, then the image f[s] is pairwise under r iff s is pairwise under r on f.

Русский

Если f инъективна на s, то образ f[s] попарно относительно r тогда и только тогда, когда s попарно относительно r через f.

LaTeX

$$(f '' s).Pairwise r \\iff s.Pairwise (r on f)$$

Lean4

/-- See also `Set.Pairwise.image`. -/
theorem pairwise_image {s : Set ι} (h : s.InjOn f) : (f '' s).Pairwise r ↔ s.Pairwise (r on f) := by
  simp +contextual [h.eq_iff, Set.Pairwise]

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