le_sSup_of_le

Mathlib.Order.CompleteLattice.Defs

URI: https://scilib.ai/kg/mathlib#le_sSup_of_le

English

If b ≤ sSup s for some b ∈ s, and a ≤ b, then a ≤ sSup s.

Русский

Если b ≤ sSup s для некоторого b ∈ s и a ≤ b, тогда a ≤ sSup s.

LaTeX

$$$ b\in s \land b \le sSup\, s \Rightarrow a \le b \Rightarrow a \le sSup\, s $$$

Lean4

theorem le_sSup_of_le (hb : b ∈ s) (h : a ≤ b) : a ≤ sSup s :=
  le_trans h (le_sSup hb)

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

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

Разделы

Аффилиация

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