Theorem Set.mem_bihimp_iff

Modification history

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