ext

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.ext

English

Two sublattices are equal if they have exactly the same elements.

Русский

Две подрешетки равны, если у них совпадают все элементы.

LaTeX

$$$ (\\forall x, x \\in L \\iff x \\in M) \\Rightarrow L = M $$$

Lean4

/-- Two sublattices are equal if they have the same elements. -/
theorem ext : (∀ a, a ∈ L ↔ a ∈ M) → L = M :=
  SetLike.ext

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

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

Разделы

Аффилиация

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