sInf — Mathlib

English

If a family {f_i} of functions f_i: α → β consists of antitone maps, then their pointwise infimum g(a) = inf_i f_i(a) is antitone in a.

Русский

Если семейство функций {f_i} с отображениями f_i: α → β состоит из антимонотонных отображений, то их точечный инфимум антимонотонен по a.

LaTeX

$$If ∀ i, f_i is Antitone, then Antitone( iInf_i f_i ).$$

Lean4

protected theorem sInf (hs : ∀ f ∈ s, Antitone f) : Antitone (sInf s) := fun _ _ h ↦ iInf_mono fun f ↦ hs f f.2 h

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