symm

Mathlib.Analysis.AbsoluteValue.Equivalence

URI: https://scilib.ai/kg/mathlib#AbsoluteValue.IsEquiv.symm

English

If h is an equivalence from v to w, then there is an inverse equivalence from w to v.

Русский

Если h — эквивалентность от v к w, то существует обратная эквивалентность от w к v.

LaTeX

$$$\\forall h:\\, v.IsEquiv w,\\; w.IsEquiv v$$$

Lean4

theorem symm (h : v.IsEquiv w) : w.IsEquiv v := fun _ _ ↦ (h _ _).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru