fuzzy_congr

Mathlib.SetTheory.PGame.Order

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

← MathLib Explorer

English

If x1 ≈ x2 and y1 ≈ y2, then x1 ‖ y1 iff x2 ‖ y2.

Русский

Если x1 ≈ x2 и y1 ≈ y2, то x1 ‖ y1 эквивалентно x2 ‖ y2.

LaTeX

$$$(x_1 \approx x_2) \Rightarrow (y_1 \approx y_2) \Rightarrow (x_1 \|\| y_1 \iff x_2 \|\| y_2)$$$

Lean4

theorem fuzzy_congr {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ ‖ y₁ ↔ x₂ ‖ y₂ :=
  show _ ∧ _ ↔ _ ∧ _ by rw [lf_congr hx hy, lf_congr hy hx]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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