Theorem: Collection.set_empty (Logic/Vorspiel/Collection.lean)

State before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
⊢ set ∅ = ∅
Tactic:
ext
State after:
case h
β : Type u_1
α : Type u_2
inst✝ : Collection β α
x✝ : β
⊢ x✝ ∈ set ∅ ↔ x✝ ∈ ∅

State before:
case h
β : Type u_1
α : Type u_2
inst✝ : Collection β α
x✝ : β
⊢ x✝ ∈ set ∅ ↔ x✝ ∈ ∅
Tactic:
simp [set]
State after:
no goals