lt_inf'_iff — Mathlib

English

Let s be nonempty finite subset of α and f: ι → α. Then a < s.inf' H f iff ∀ i ∈ s, a < f(i).

Русский

Пусть s непустое конечное подмножество и f: ι → α. Тогда a < s.inf' H f эквивалентно для всех i ∈ s выполняется a < f(i).

LaTeX

$$$a < s.inf' H f \iff \forall i \in s, a < f(i).$$$

Lean4

@[simp]
theorem lt_inf'_iff : a < s.inf' H f ↔ ∀ i ∈ s, a < f i :=
  sup'_lt_iff (α := αᵒᵈ) H

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