fuzzy_of_equiv_of_fuzzy

Mathlib.SetTheory.PGame.Order

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.fuzzy_of_equiv_of_fuzzy

English

If x ≈ y and y ‖ z then x ‖ z.

Русский

Если x ≈ y и y ‖ z, то x ‖ z.

LaTeX

$$$(x \approx y) \land (y \|\| z) \Rightarrow (x \|\| z)$$$

Lean4

@[trans]
theorem fuzzy_of_equiv_of_fuzzy {x y z : PGame} (h₁ : x ≈ y) (h₂ : y ‖ z) : x ‖ z :=
  (fuzzy_congr_left h₁).2 h₂

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

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

Разделы

Аффилиация

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