covariant_of_const — Mathlib

English

Dual of Covariant: if f is antitone, then f(μ m x) is antitone in x.

Русский

Двойственность к ковариантности: если f антитонна, то f(μ m x) антитонна по x.

LaTeX

$$$\text{Antitone}(f) \to \text{Antitone}(f(\mu m \cdot ))$$$

Lean4

/-- Dual of `Monotone.covariant_of_const` -/
theorem covariant_of_const [CovariantClass M N μ (· ≤ ·)] (hf : Antitone f) (m : M) : Antitone (f <| μ m ·) :=
  hf.comp_monotone <| Covariant.monotone_of_const m

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