subtypeEquiv_symm — Mathlib

English

The inverse of subtypeEquiv is the subtypeEquiv of the inverse equivalence with an appropriate predicate relation.

Русский

Обратное к subtypeEquiv есть subtypeEquiv от обратной эквивалентности с подходящим отношением предикатов.

LaTeX

$$$$ (e.subtypeEquiv h).symm = e.symm.subtypeEquiv (\\text{by auxiliary lemma}). $$$$

Lean4

@[simp]
theorem subtypeEquiv_symm {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ a : α, p a ↔ q (e a)) :
    (e.subtypeEquiv h).symm = e.symm.subtypeEquiv (by as_aux_lemma => grind) :=
  rfl

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