neLocus_comm

Mathlib.Data.DFinsupp.NeLocus

URI: https://scilib.ai/kg/mathlib#DFinsupp.neLocus_comm

English

The difference locus is symmetric between the two functions: swapping f and g leaves the locus unchanged.

Русский

Локус различий симметричен по отношению к переходу f ↔ g: локус не меняется при перестановке f и g.

LaTeX

$$$ f \neLocus g = g \neLocus f $$$

Lean4

theorem neLocus_comm : f.neLocus g = g.neLocus f := by simp_rw [neLocus, Finset.union_comm, ne_comm]

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

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

Разделы

Аффилиация

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