preimage_eq_empty

Mathlib.Data.Set.Image

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

English

If s is disjoint from the range of f, then the preimage f^{-1}(s) is empty.

Русский

Если s дизjoint с образом f, то прообраз f^{-1}(s) пуст.

LaTeX

$$$\operatorname{Disjoint}(s, \operatorname{range}(f)) \Rightarrow f^{-1}(s) = \emptyset$$$

Lean4

theorem preimage_eq_empty {s : Set β} (h : Disjoint s (range f)) : f ⁻¹' s = ∅ := by simpa using h.preimage f

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

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

Разделы

Аффилиация

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