iSup_le

Mathlib.Order.CompletePartialOrder

URI: https://scilib.ai/kg/mathlib#Directed.iSup_le

English

If f: ι → α is directed and f(i) ≤ a for all i, then ⨆ i, f(i) ≤ a.

Русский

Если f: ι → α направлено и ∀ i, f(i) ≤ a, тогда ⨆ i, f(i) ≤ a.

LaTeX

$$$\text{Directed}(\le)\ f \rightarrow (\forall i, \ f(i) \le a) \rightarrow \bigvee_{i} f(i) \le a$$$

Lean4

protected theorem iSup_le (hf : Directed (· ≤ ·) f) (ha : ∀ i, f i ≤ a) : ⨆ i, f i ≤ a :=
  hf.directedOn_range.sSup_le <| Set.forall_mem_range.2 ha

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

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

Разделы

Аффилиация

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