comm

Mathlib.SetTheory.ZFC.PSet

URI: https://scilib.ai/kg/mathlib#PSet.Equiv.comm

English

Equiv x y is equivalent to Equiv y x.

Русский

Эквивалентность x y равносильна Equiv y x.

LaTeX

$$Equiv x y ↔ Equiv y x$$

Lean4

protected theorem comm {x y} : Equiv x y ↔ Equiv y x :=
  ⟨Equiv.symm, Equiv.symm⟩

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

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

Разделы

Аффилиация

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