Theorem Set.pairwise_iff_of_refl

Modification history

2026-08-21 01:13
Mathlib/Data/Set/Pairwise/Basic.lean
chore: deduplicate `Set.pairwise_iff_of_refl` and add aliases (#42807) …
Modified Set.pairwise_iff_of_reflView on Github →
2026-01-09 08:53
Mathlib/Data/Set/Pairwise/Basic.lean
chore(Order/Defs/Unbundled): deprecate `IsRefl` in favor of core's `Std.Refl` (#33755)
Modified Set.pairwise_iff_of_reflView on Github →
2022-12-24 11:23
Mathlib/Data/Set/Pairwise.lean
feat: port Data.Set.Pairwise (#1175)
Added Set.pairwise_iff_of_reflView on Github →