mk_eq_bot_iff — Mathlib

English

For p ∈ f.invtSubmodule, the element ⟨p, hp⟩ of the invariant-submodule structure is bottom iff p = ⊥.

Русский

Для p ∈ f.invtSubmodule элемент ⟨p, hp⟩ равен ⊥ тогда и только тогда, когда p = ⊥.

LaTeX

$$$\text{If } p\in f.invtSubmodule,\; (⟨p,\,hp\rangle : f.invtSubmodule) = ⊥ \iff p=⊥$$$

Lean4

protected theorem mk_eq_bot_iff {p : Submodule R M} (hp : p ∈ f.invtSubmodule) :
    (⟨p, hp⟩ : f.invtSubmodule) = ⊥ ↔ p = ⊥ :=
  Subtype.mk_eq_bot_iff (by simp [invtSubmodule]) _

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