iSup_const_mono

Mathlib.Order.CompleteLattice.Basic

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

English

Let a be fixed and h : ι → ι'. Then ⨆_{ι} a ≤ ⨆_{ι'} a.

Русский

Пусть a фиксировано; тогда ⨆_ι a ≤ ⨆_{ι'} a.

LaTeX

$$$\\\\forall a, \\\\left( h : ι \\\\to ι' \\\\right) \\\\Rightarrow \\\\bigvee_{x:ι} a \\\\le \\\\bigvee_{x:ι'} a$$$

Lean4

theorem iSup_const_mono (h : ι → ι') : ⨆ _ : ι, a ≤ ⨆ _ : ι', a :=
  iSup_le <| le_iSup _ ∘ h

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

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

Разделы

Аффилиация

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