monotone — Mathlib

English

If f is antitone on s, then the composition f ∘ Subtype.val is antitone on s.

Русский

Если f анти монотонна на s, то f ∘ Subtype.val на s антимонотонна.

LaTeX

$$$\operatorname{AntitoneOn}(f,s) \Rightarrow \operatorname{Antitone}(f \circ \operatorname{Subtype.val} : s \to \beta)$$$

Lean4

protected theorem _root_.AntitoneOn.monotone (h : AntitoneOn f s) : Antitone (f ∘ Subtype.val : s → β) := fun x y hle =>
  h x.coe_prop y.coe_prop hle

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