neLocus_comm

Mathlib.Data.Finsupp.NeLocus

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

English

neLocus is symmetric: f.neLocus g = g.neLocus f.

Русский

neLocus симметрично: f.neLocus g = g.neLocus f.

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