map_top

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#Ideal.map_top

English

x ∈ comap f K iff f x ∈ K (simp).

Русский

x принадлежит обратному образу, тогда как f x принадлежит K.

LaTeX

$$$ x \in \operatorname{comap} f K \iff f x \in K $$$

Lean4

theorem map_top : map f ⊤ = ⊤ :=
  (eq_top_iff_one _).2 <| subset_span ⟨1, trivial, map_one f⟩

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

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

Разделы

Аффилиация

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