inf_le_iff

Mathlib.Data.Finset.Lattice.Fold

URI: https://scilib.ai/kg/mathlib#Finset.inf_le_iff

English

For any a strictly below top, s.inf f ≤ a iff there exists b ∈ s with f(b) ≤ a.

Русский

Пусть a < ⊤. Тогда s.inf f ≤ a эквивалентно существованию b ∈ s такое, что f(b) ≤ a.

LaTeX

$$$a < \top \Rightarrow (s.inf f \le a \iff \exists b \in s, f(b) \le a)$$$

Lean4

@[simp]
protected theorem inf_le_iff (ha : a < ⊤) : s.inf f ≤ a ↔ ∃ b ∈ s, f b ≤ a :=
  @Finset.le_sup_iff αᵒᵈ _ _ _ _ _ _ ha

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

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

Разделы

Аффилиация

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