range_le_ker_iff — Mathlib

English

If range f = ⊤, then comap f p ≤ comap f p' iff p ≤ p'.

Русский

Если диапазон = ⊤, то comap f p ≤ comap f p' эквивалентно p ≤ p'.

LaTeX

$$$\operatorname{comap} f p \le \operatorname{comap} f p' \iff p \le p'$ (при $\operatorname{range} f = \top$)$$

Lean4

theorem range_le_ker_iff {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} : range f ≤ ker g ↔ (g.comp f : M →ₛₗ[τ₁₃] M₃) = 0 :=
  ⟨fun h => ker_eq_top.1 <| eq_top_iff'.2 fun _ => h <| ⟨_, rfl⟩, fun h x hx =>
    mem_ker.2 <| Exists.elim hx fun y hy => by rw [← hy, ← comp_apply, h, zero_apply]⟩

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