ker_inf_lt_ker_inf_of_map_eq_of_lt

English

If f is surjective and h: p ⋖ q, then p.comap f ⋖ q.comap f.

Русский

Если f сюръективно и h: p ⋖ q, то p.comap f ⋖ q.comap f.

LaTeX

$$$\operatorname{comap}_f p \;\lessdot\; \operatorname{comap}_f q$$$

Lean4

theorem _root_.LinearMap.ker_inf_lt_ker_inf_of_map_eq_of_lt {f : F} (hab : p < p')
    (q : Submodule.map f p = Submodule.map f p') : LinearMap.ker f ⊓ p < LinearMap.ker f ⊓ p' :=
  map_strict_mono_or_ker_sup_lt_ker_sup f hab |>.resolve_left q.not_lt

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