kernImage_empty

Mathlib.Data.Set.Lattice.Image

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

English

The kernImage of the empty set is the complement of the range: kernImage f ∅ = (range f)^c.

Русский

KernImage пустого множества равен дополнению диапазона: kernImage f ∅ = (range f)^c.

LaTeX

$$$\\mathrm{kernImage}\\, f\\, \\emptyset = (\\mathrm{range}\\, f)^c$$$

Lean4

theorem kernImage_empty : kernImage f ∅ = (range f)ᶜ := by rw [kernImage_eq_compl, compl_empty, image_univ]

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

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

Разделы

Аффилиация

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