iInf_const_mono

Mathlib.Order.CompleteLattice.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem iInf_const_mono (h : ι' → ι) : ⨅ _ : ι, a ≤ ⨅ _ : ι', a :=
  le_iInf <| iInf_le _ ∘ h

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

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

Разделы

Аффилиация

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