sInf_apply — Mathlib

English

The infimum over a set of order-preserving maps, applied to an argument, equals the infimum over the set of maps of their values at that argument.

Русский

Инфимум над множеством отображений сохраняется при применении к аргументу: sInf(s)(x) = inf_{f∈s} f(x).

LaTeX

$$$sInf\; s\; x = \inf_{f \in s} (f\,x).$$$

Lean4

@[simp]
theorem sInf_apply [CompleteLattice β] (s : Set (α →o β)) (x : α) : sInf s x = ⨅ f ∈ s, (f :) x :=
  rfl

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