ne_bot_of_map_ne_bot — Mathlib

English

If the image under map f of I is not the bottom ideal, then I itself is not the bottom ideal: map f I ≠ ⊥ ⇒ I ≠ ⊥.

Русский

Если образ через map f идеала I не равен нулю, то сам I не нулевой: map f I ≠ ⊥ ⇒ I ≠ ⊥.

LaTeX

$$$\\operatorname{map} f(I) \\neq \\bot \\;\\Rightarrow\\; I \\neq \\bot$$$

Lean4

theorem ne_bot_of_map_ne_bot (hI : map f I ≠ ⊥) : I ≠ ⊥ := fun h =>
  hI (Eq.mpr (congrArg (fun I ↦ map f I = ⊥) h) map_bot)

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