Commit 2026-06-02 04:58 75a3ec64

feat: x ∈ s ⇨ t ↔ x ∈ s → x ∈ t (#40133) We prove some trivial characterizations of Heyting implication and bi-implication on sets.