fuzzy_congr_right

Mathlib.SetTheory.PGame.Order

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

English

If y1 ≈ y2 then x ‖ y1 iff x ‖ y2 for any x.

Русский

Если y1 ≈ y2, то x ‖ y1 эквивалентно x ‖ y2 для любого x.

LaTeX

$$$(y_1 \approx y_2) \Rightarrow (x \|\| y_1 \iff x \|\| y_2)$$$

Lean4

theorem fuzzy_congr_right {x y₁ y₂ : PGame} (hy : y₁ ≈ y₂) : x ‖ y₁ ↔ x ‖ y₂ :=
  fuzzy_congr equiv_rfl hy

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

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

Разделы

Аффилиация

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