bihimp_eq_left

Mathlib.Order.SymmDiff

URI: https://scilib.ai/kg/mathlib#bihimp_eq_left

English

The equality bihimp a b = a equals bihimp b with ⊤ relation implies a is unaffected; specifically bihimp a b = a implies b = ⊤.

Русский

Если bihimp a b = a, то b = ⊤.

LaTeX

$$$ bihimp(a, b) = a \Rightarrow b = \top $$$

Lean4

@[simp]
theorem bihimp_eq_left : a ⇔ b = a ↔ b = ⊤ :=
  @symmDiff_eq_left αᵒᵈ _ _ _

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

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

Разделы

Аффилиация

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