sInf — Mathlib

English

The infimum of a set S of filters is the supremum of their lower bounds: sInf(S) = sSup(lowerBounds S).

Русский

Наибольшая нижняя граница множества фильтров S равна супремуму их нижних границ: sInf(S) = sSup(lowerBounds S).

LaTeX

$$$\\operatorname{sInf}(S) = \\operatorname{sSup}(\\operatorname{lowerBounds} S)$$$

Lean4

/-- Infimum of a set of filters.
This definition is marked as irreducible
so that Lean doesn't try to unfold it when unifying expressions. -/
@[irreducible]
protected def sInf (s : Set (Filter α)) : Filter α :=
  sSup (lowerBounds s)

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