preimage_eq_preimage' — Mathlib

English

For s,t ⊆ range f, f^{-1}(s) = f^{-1}(t) iff s = t.

Русский

Для подмножеств s,t ⊆ range(f) выполняется f^{-1}(s) = f^{-1}(t) тогда и только тогда, когда s = t.

LaTeX

$$$ f^{-1}(s) = f^{-1}(t) \\iff s = t, \\quad s,t \\subseteq \\mathrm{range}(f). $$$

Lean4

theorem preimage_eq_preimage' {s t : Set α} {f : β → α} (hs : s ⊆ range f) (ht : t ⊆ range f) :
    f ⁻¹' s = f ⁻¹' t ↔ s = t := by
  constructor
  · intro h
    apply Subset.antisymm
    · rw [← preimage_subset_preimage_iff hs, h]
    · rw [← preimage_subset_preimage_iff ht, h]
  rintro rfl;
  rfl
    -- Not `@[simp]` since `simp` can prove this.

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