ih1_swap

Mathlib.SetTheory.Surreal.Multiplication

URI: https://scilib.ai/kg/mathlib#Surreal.Multiplication.ih1_swap

← MathLib Explorer

English

IH1 is preserved under swapping the operands: IH1 y x follows from IH1 x y.

Русский

IH1 сохраняется при перестановке аргументов: IH1 y x следует из IH1 x y.

LaTeX

$$$IH1\\ (y,x) \\text{ follows from } IH1\\ (x,y)$$$

Lean4

theorem ih1_swap (ih : ∀ a, ArgsRel a (Args.P1 x y) → P124 a) : IH1 y x :=
  ih1 <| by
    simp_rw [ArgsRel, InvImage, Args.toMultiset, Multiset.pair_comm] at ih ⊢
    exact ih

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

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

Разделы

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

Аффилиация

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