α : Type u_1
β : Type ?u.10878
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
this : ChainClosure r (⋃₀ ∅)
⊢ ChainClosure r ∅
α : Type u_1
β : Type ?u.10878
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
⊢ ChainClosure r ∅
have : ChainClosure r (⋃₀∅) := ChainClosure.union fun a h => False.rec h
no goals
α : Type u_1
β : Type ?u.10878
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
this : ChainClosure r (⋃₀ ∅)
⊢ ChainClosure r ∅
simpa using this