le_ker_iff — Mathlib

English

For a LieHom f and a LieIdeal I, I ≤ ker f if and only if ∀ x ∈ I, f(x) = 0.

Русский

Для гомоморфизма Ли f и идеала I верно: I ≤ ker f тогда и только тогда, когда для всех x ∈ I выполняется f(x) = 0.

LaTeX

$$$I \\le f.ker \\iff \\forall x \\in I, f(x)=0$$$

Lean4

theorem le_ker_iff : I ≤ f.ker ↔ ∀ x, x ∈ I → f x = 0 :=
  by
  constructor <;> intro h x hx
  · specialize h hx; rw [mem_ker] at h; exact h
  · rw [mem_ker]; apply h x hx

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