Theorem Finset.mem_bihimp_iff

Modification history

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