trans

Mathlib.Data.Subtype

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

English

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

Русский

Если s эквивалентно t, а t эквивалентно u, то s эквивалентно u.

LaTeX

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

Lean4

protected theorem trans {s t u : Subtype p} (h₁ : s ≈ t) (h₂ : t ≈ u) : s ≈ u :=
  Setoid.trans h₁ h₂

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

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

Разделы

Аффилиация

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