ker_liftQ_eq_bot — Mathlib

English

If ker f ≤ p, then ker (p.liftQ f h) = ⊥. In words, lifting along p introduces no new kernel under the assumption ker f lies inside p.

Русский

Если ker f ≤ p, то ker (p.liftQ f h) = ⊥. Иначе говоря, подъём вдоль p не добавляет нулевых элементов в ядро при условии, что ядро f лежит внутри p.

LaTeX

$$$$ \\ker (p.liftQ f h) = \\bot. $$$$

Lean4

theorem ker_liftQ_eq_bot (f : M →ₛₗ[τ₁₂] M₂) (h) (h' : ker f ≤ p) : ker (p.liftQ f h) = ⊥ := by
  rw [ker_liftQ, le_antisymm h h', mkQ_map_self]

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