mem_principal

Mathlib.Order.Ideal

URI: https://scilib.ai/kg/mathlib#Order.Ideal.mem_principal

English

x ∈ principal y iff x ≤ y.

Русский

x принадлежит principal y тогда и только тогда, когда x ≤ y.

LaTeX

$$x \in principal y \iff x \le y$$

Lean4

@[simp]
theorem mem_principal : x ∈ principal y ↔ x ≤ y :=
  Iff.rfl

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

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

Разделы

Аффилиация

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