le_inf_iff

Mathlib.Data.Finset.Lattice.Fold

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

English

For all a ∈ α, a ≤ s.inf f if and only if a ≤ f(b) for all b ∈ s.

Русский

Для каждого a в α выполняется a ≤ s.inf f тогда и только тогда, когда a ≤ f(b) для всех b ∈ s.

LaTeX

$$$ a \le s.inf f \quad\Leftrightarrow\quad \forall b \in s,\ a \le f(b) $$$

Lean4

@[simp]
protected theorem le_inf_iff {a : α} : a ≤ s.inf f ↔ ∀ b ∈ s, a ≤ f b :=
  @Finset.sup_le_iff αᵒᵈ _ _ _ _ _ _

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

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

Разделы

Аффилиация

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