eq_bot_iff — Mathlib

English

Protected version: p = ⊥ iff for all x ∈ p, x = 0 (within a protected context).

Русский

Защищённая версия: p = ⊥ эквивалентно тому, что для каждого x ∈ p верно x = 0 (в защищённом контексте).

LaTeX

$$p = ⊥ ↔ ∀ x ∈ p, x = 0$$

Lean4

protected theorem eq_bot_iff (p : Submodule R M) : p = ⊥ ↔ ∀ x ∈ p, x = (0 : M) :=
  ⟨fun h ↦ h.symm ▸ fun _ hx ↦ (mem_bot R).mp hx, fun h ↦ eq_bot_iff.mpr fun x hx ↦ (mem_bot R).mpr (h x hx)⟩

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