le_Ici

Mathlib.Order.UpperLower.Principal

URI: https://scilib.ai/kg/mathlib#UpperSet.le_Ici

English

For any upper set s and any element a, s is contained in the principal upper set Ici(a) if and only if a belongs to s.

Русский

Для любой верхней области s и любого элемента a верно: s ≤ Ici(a) тогда и только тогда, когда a ∈ s.

LaTeX

$$$s \le Ici(a) \iff a \in s$$$

Lean4

@[simp]
theorem le_Ici : s ≤ Ici a ↔ a ∈ s :=
  ⟨fun h ↦ h le_rfl, fun ha ↦ s.upper.Ici_subset ha⟩

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

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

Разделы

Аффилиация

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