preimage_eq_iff_eq_image

Mathlib.Data.Set.Image

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

← MathLib Explorer

English

If f is bijective, then f^{-1}(s) = t iff s = f''t for any sets s,t.

Русский

Если f биективна, то f^{-1}(s) = t тогда и только тогда, когда s = f''(t) для любых множеств s,t.

LaTeX

$$$f$ is bijective implies $f^{-1}(s)=t \iff s=f''t$$$

Lean4

theorem preimage_eq_iff_eq_image {f : α → β} (hf : Bijective f) {s t} : f ⁻¹' s = t ↔ s = f '' t := by
  rw [← image_eq_image hf.1, hf.2.image_preimage]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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