preimage_eq_univ_iff

Mathlib.Data.Set.Image

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

English

f^{-1}(s) = univ iff range f ⊆ s.

Русский

Преобразование по образу: f^{-1}(s) = univ тогда и только тогда, когда range f ⊆ s.

LaTeX

$$$ f^{-1}(s) = \\operatorname{univ} \\iff \\operatorname{range} f \\subseteq s $$$

Lean4

@[simp]
theorem preimage_eq_univ_iff {f : α → β} {s} : f ⁻¹' s = univ ↔ range f ⊆ s := by
  rw [← univ_subset_iff, ← image_subset_iff, image_univ]

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

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

Разделы

Аффилиация

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