setCongr — Mathlib

English

If s = t, there is an order isomorphism between s and t, given by the canonical set-congruence.

Русский

Если множества s и t равны, существует изоморфизм порядка между s и t, задаваемый каноническим конгруэнсом множеств.

LaTeX

$$$s \simeq_o t \text{ whenever } s=t$$$

Lean4

/-- Order isomorphism between two equal sets. -/
@[simps! apply symm_apply]
def setCongr (s t : Set α) (h : s = t) : s ≃o t
    where
  toEquiv := Equiv.setCongr h
  map_rel_iff' := Iff.rfl

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