Theorem Set.Pairwise.insert_of_symm_of_refl

Modification history

2026-09-07 07:56
Mathlib/Data/Set/Pairwise/Basic.lean
refactor: use `Set.Pairwise s Commute` for commutativity of subobject closures (#42804) …
Added Set.Pairwise.insert_of_symm_of_reflView on Github →