Theorem Set.mem_himp_iff

Modification history

2026-06-02 04:58
Mathlib/Order/BooleanAlgebra/Set.lean
feat: `x ∈ s ⇨ t ↔ x ∈ s → x ∈ t` (#40133) …
Added Set.mem_himp_iffView on Github →