principal_le_iff

Mathlib.Order.Ideal

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

English

principal x ≤ I if and only if x ∈ I.

Русский

principal x ≤ I тогда и только тогда, когда x ∈ I.

LaTeX

$$principal x \le I \iff x \in I$$

Lean4

@[simp]
theorem principal_le_iff : principal x ≤ I ↔ x ∈ I :=
  ⟨fun h ↦ h le_rfl, fun hx _ hy ↦ I.lower hy hx⟩

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

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

Разделы

Аффилиация

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