ker_eq_top — Mathlib

English

If f ≠ 0 and the supremum of a family of submodules equals ⊤, there exists a member where f is nonzero on the subtype.

Русский

Если f ≠ 0 и супремум семейства подподмодулей равен ⊤, существует элемент, на котором f не нулевой на подтипе.

LaTeX

$$∃ s ∈ S, f ∘ s.subtype ≠ 0 (given sSup S = ⊤ and f ≠ 0)$$

Lean4

@[simp]
theorem ker_eq_top {f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊤ ↔ f = 0 :=
  ⟨fun h => ext fun _ => mem_ker.1 <| h.symm ▸ trivial, fun h => h.symm ▸ ker_zero⟩

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