subsingleton_iff_eq_bot — Mathlib

English

For any submodule p of M, p is a subsingleton if and only if p = ⊥.

Русский

Для любого подмодуля p пространства M выполняется: p — это единичный тип тогда и только тогда, когда p = ⊥.

LaTeX

$$$\text{Subsingleton}(p) \iff p = \bot$$$

Lean4

theorem subsingleton_iff_eq_bot : Subsingleton p ↔ p = ⊥ :=
  by
  rw [subsingleton_iff, Submodule.eq_bot_iff]
  refine ⟨fun h x hx ↦ by simpa using h ⟨x, hx⟩ ⟨0, p.zero_mem⟩, fun h ⟨x, hx⟩ ⟨y, hy⟩ ↦ by simp [h x hx, h y hy]⟩

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