bot_of_map_eq_bot — Mathlib

English

If f is injective and I.map f = {0}, then I = {0}.

Русский

Если f инъективен и образ I через f равен нулю, то I тривиален.

LaTeX

$$$\text{Injective}(f) \Rightarrow I.map f = \{0\} \Rightarrow I = \{0\}$$$

Lean4

theorem bot_of_map_eq_bot {I : LieIdeal R L} (h₁ : Function.Injective f) (h₂ : I.map f = ⊥) : I = ⊥ :=
  by
  rw [← f.ker_eq_bot, LieHom.ker] at h₁
  rw [eq_bot_iff, map_le_iff_le_comap, h₁] at h₂
  rw [eq_bot_iff]; exact h₂

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