iInf — Mathlib

English

If a family {f_i} of functions f_i: α → β consists of antitone maps, then the indexed infimum iInf_i f_i is antitone.

Русский

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

LaTeX

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

Lean4

protected theorem iInf (hf : ∀ i, Monotone (f i)) : Monotone (⨅ i, f i) :=
  Monotone.sInf (by simpa)

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