le_sInf_iff — Mathlib

English

In a complete semilattice with infimum, a is below the infimum of a set s if and only if a is below every element of s.

Русский

В полупорядке, в котором существует наиб. нижняя граница, элемент a ниже наиб. нижней границы множества s тогда и только тогда, когда a ниже любого элемента из s.

LaTeX

$$$a \le s\!\Inf s \;\iff\; \forall b \in s,\; a \le b$$$

Lean4

@[simp]
theorem le_sInf_iff : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b :=
  le_isGLB_iff (isGLB_sInf s)

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