α : Type u_1
β : Type ?u.8808
s : Set (Setoid α)
⊢ (EqvGen.Setoid fun x y => ∃ r, r ∈ s ∧ Rel r x y) = EqvGen.Setoid (⨆ (a : Setoid α) (_ : a ∈ s), Rel a)
α : Type u_1
β : Type ?u.8808
s : Set (Setoid α)
⊢ sSup s = EqvGen.Setoid (sSup (Rel '' s))
rw [sSup_eq_eqvGen, sSup_image]
case e_r.h.h.a
α : Type u_1
β : Type ?u.8808
s : Set (Setoid α)
x y : α
⊢ (∃ r, r ∈ s ∧ Rel r x y) ↔ iSup (fun a => ⨆ (_ : a ∈ s), Rel a) x y
α : Type u_1
β : Type ?u.8808
s : Set (Setoid α)
⊢ (EqvGen.Setoid fun x y => ∃ r, r ∈ s ∧ Rel r x y) = EqvGen.Setoid (⨆ (a : Setoid α) (_ : a ∈ s), Rel a)
congr with (x y)
no goals
case e_r.h.h.a
α : Type u_1
β : Type ?u.8808
s : Set (Setoid α)
x y : α
⊢ (∃ r, r ∈ s ∧ Rel r x y) ↔ iSup (fun a => ⨆ (_ : a ∈ s), Rel a) x y
simp only [iSup_apply, iSup_Prop_eq, exists_prop]