eq_top_iff'

Mathlib.Algebra.Module.Submodule.Lattice

URI: https://scilib.ai/kg/mathlib#Submodule.eq_top_iff'

English

For any p, p = ⊤ iff ∀ x, x ∈ p.

Русский

Для любого p верно: p = ⊤ тогда и только тогда, когда для всех x выполняется x ∈ p.

LaTeX

$$$p = \top \iff \forall x, x \in p$$$

Lean4

theorem eq_top_iff' {p : Submodule R M} : p = ⊤ ↔ ∀ x, x ∈ p :=
  eq_top_iff.trans ⟨fun h _ ↦ h trivial, fun h x _ ↦ h x⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru