inverse_compare — Mathlib

English

The composition of compare in opposite order yields the identity.

Русский

Произведение сравнения в противном порядке даёт тождество.

LaTeX

$$$ pkg.compare pkg' \circ pkg'.compare pkg = id $$$

Lean4

theorem inverse_compare : pkg.compare pkg' ∘ pkg'.compare pkg = id :=
  by
  have uc := pkg.uniformContinuous_compare pkg'
  have uc' := pkg'.uniformContinuous_compare pkg
  apply pkg'.funext (uc.comp uc').continuous continuous_id
  intro a
  rw [comp_apply, pkg'.compare_coe pkg, pkg.compare_coe pkg']
  rfl

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