preimage_eq_preimage

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.preimage_eq_preimage

English

For surjective f: β → α, f^{-1}(s) = f^{-1}(t) iff s = t.

Русский

Для сюръективного f: β → α верно f^{-1}(s) = f^{-1}(t) тогда и только тогда, когда s = t.

LaTeX

$$$$ f^{-1}(s) = f^{-1}(t) \iff s = t \quad \text{if } f \text{ is surjective}. $$$$

Lean4

@[simp]
theorem preimage_eq_preimage {f : β → α} (hf : Surjective f) : f ⁻¹' s = f ⁻¹' t ↔ s = t :=
  (preimage_injective.mpr hf).eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru