image_eq_iff_eq — Mathlib

English

Let e: α ≃ β be a bijection. For subsets s,t ⊆ α, the images satisfy e''s = e''t if and only if s = t.

Русский

Пусть e: α ≃ β — биекция. Для подмножеств s, t ⊆ α выполняется e[s] = e[t] тогда и только тогда, когда s = t.

LaTeX

$$$ e'' s = e'' t \\iff s = t $$$

Lean4

@[simp]
theorem image_eq_iff_eq {α β} (e : α ≃ β) (s t : Set α) : e '' s = e '' t ↔ s = t :=
  image_eq_image e.injective

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