csInf_eq_min'

Mathlib.Order.ConditionallyCompleteLattice.Finset

URI: https://scilib.ai/kg/mathlib#Finset.Nonempty.csInf_eq_min'

English

For a nonempty finite set, the Infimum equals its minimum.

Русский

Для непустого конечного множества инфиму́м равен его минимуму.

LaTeX

$$$\forall s:\ Finset\ α, s.Nonempty \Rightarrow sInf\ s.toSet = s.min' s.Nonempty$$$

Lean4

theorem csInf_eq_min' {s : Finset α} (h : s.Nonempty) : sInf ↑s = s.min' h :=
  @Finset.Nonempty.csSup_eq_max' αᵒᵈ _ s h

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

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

Разделы

Аффилиация

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