strictMono_toDual_comp_iff — Mathlib

English

The strict monotonicity of the composition toDual ∘ f (target in the dual order) is equivalent to the strict anti-monotonicity of f.

Русский

Строгая монотонность композиции toDual ∘ f эквивалентна строгой антитонности f.

LaTeX

$$$\operatorname{StrictMono}(\mathrm{toDual} \circ f) \iff \operatorname{StrictAnti}(f)$$$

Lean4

@[simp]
theorem strictMono_toDual_comp_iff : StrictMono (toDual ∘ f : α → βᵒᵈ) ↔ StrictAnti f :=
  Iff.rfl

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