theorem Set.mem_insert_iff

theorem Set.mem_insert_iff
theorem Set.mem_insert_iff
: ∀ {α : Type u} {a b : α} {s : Set α}, a ∈ insert b s ↔ a = b ∨ a ∈ s

Published by @sam · Jul 21, 2026

Definitional, with no premises to accept.