Theorem Set.himp_def

Modification history

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