fuzzy_congr_left

Mathlib.SetTheory.PGame.Order

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

English

If x1 ≈ x2 then x1 ‖ y iff x2 ‖ y for any y.

Русский

Если x1 ≈ x2, то x1 ‖ y эквивалентно x2 ‖ y для любого y.

LaTeX

$$$(x_1 \approx x_2) \Rightarrow (x_1 \|\| y \iff x_2 \|\| y)$$$

Lean4

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

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

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

Разделы

Аффилиация

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