inf'_le_iff — Mathlib

English

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

Русский

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

LaTeX

$$$s.inf' H f \le a \iff \exists i \in s, f(i) \le a.$$$

Lean4

@[simp]
theorem inf'_le_iff : s.inf' H f ≤ a ↔ ∃ i ∈ s, f i ≤ a :=
  le_sup'_iff (α := αᵒᵈ) H

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