Theorem Set.mem_bihimp

Modification history

2026-06-02 07:58
Mathlib/Data/Set/SymmDiff.lean
feat: `x ∈ s ⇨ t ↔ x ∈ s → x ∈ t` (for finsets) (#40140) …
Deleted Set.mem_bihimpView on Github →
2026-06-02 04:58
Mathlib/Data/Set/SymmDiff.lean
feat: `x ∈ s ⇨ t ↔ x ∈ s → x ∈ t` (#40133) …
Added Set.mem_bihimpView on Github →