inf'_lt_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 < a \iff \exists i \in s, f(i) < a.$$$

Lean4

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

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