strictAnti — Mathlib

English

If f is strictly antitone on s, then the composed function f ∘ Subtype.val is strictly antitone on s.

Русский

Если f строго антитонична на s, то f ∘ Subtype.val на s строго антитонична.

LaTeX

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

Lean4

protected theorem _root_.StrictAntiOn.strictAnti (h : StrictAntiOn f s) : StrictAnti (f ∘ Subtype.val : s → β) :=
  fun x y hlt => h x.coe_prop y.coe_prop hlt

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