nontrivial_iff_ne_bot

Mathlib.Algebra.Module.Submodule.Lattice

URI: https://scilib.ai/kg/mathlib#Submodule.nontrivial_iff_ne_bot

English

Nontrivial p is equivalent to p ≠ ⊥.

Русский

Не тривиальное подмножество эквивалентно p ≠ ⊥.

LaTeX

$$$\text{Nontrivial}(p) \iff p \neq \bot$$$

Lean4

theorem nontrivial_iff_ne_bot : Nontrivial p ↔ p ≠ ⊥ := by
  rw [iff_not_comm, not_nontrivial_iff_subsingleton, subsingleton_iff_eq_bot]

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

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

Разделы

Аффилиация

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