symm

Mathlib.Data.Subtype

URI: https://scilib.ai/kg/mathlib#Subtype.symm

English

If s ≈ t in Subtype p, then t ≈ s.

Русский

Если два элемента подтипа p эквивалентны, то наоборот.

LaTeX

$$$\forall {s t : \{ a : \alpha \mid p(a) \}},\ s \approx t \Rightarrow t \approx s$$$

Lean4

protected theorem symm {s t : Subtype p} (h : s ≈ t) : t ≈ s :=
  Setoid.symm h

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

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

Разделы

Аффилиация

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