ker_liftQ_eq_bot' — Mathlib

English

A specialization: if p = ker f, then ker (p.liftQ f (le_of_eq h)) = ⊥, equivalently ker (p.liftQ f h) = ⊥.

Русский

Уточнение: если p = ker f, то ker (p.liftQ f (le_of_eq h)) = ⊥, то есть ядро подъёма равно нулю.

LaTeX

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

Lean4

theorem ker_liftQ_eq_bot' (f : M →ₛₗ[τ₁₂] M₂) (h : p = ker f) : ker (p.liftQ f (le_of_eq h)) = ⊥ :=
  ker_liftQ_eq_bot p f h.le h.ge

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