biInf_const

Mathlib.Order.CompleteLattice.Basic

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

English

If s is nonempty, then the infimum over i in s of a equals a.

Русский

Если множество s ненулевое, то инфимум по i в s от константы a равен a.

LaTeX

$$$ \\text{If } s \\text{ is nonempty, then } \\bigwedge_{i \\in s} a = a. $$$

Lean4

theorem biInf_const {a : α} {s : Set β} (hs : s.Nonempty) : ⨅ i ∈ s, a = a :=
  biSup_const (α := αᵒᵈ) hs

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

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

Разделы

Аффилиация

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