case h.h.a
α : Type u_1
β : Type ?u.2669
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ Rel (sInf s) x✝¹ x✝ ↔ sInf (Rel '' s) x✝¹ x✝
α : Type u_1
β : Type ?u.2669
s : Set (Setoid α)
⊢ Rel (sInf s) = sInf (Rel '' s)
ext
case h.h.a
α : Type u_1
β : Type ?u.2669
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ Rel (sInf s) x✝¹ x✝ ↔ ∀ (i : Setoid α), i ∈ s → Rel i x✝¹ x✝
case h.h.a
α : Type u_1
β : Type ?u.2669
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ Rel (sInf s) x✝¹ x✝ ↔ sInf (Rel '' s) x✝¹ x✝
simp only [sInf_image, iInf_apply, iInf_Prop_eq]
no goals
case h.h.a
α : Type u_1
β : Type ?u.2669
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ Rel (sInf s) x✝¹ x✝ ↔ ∀ (i : Setoid α), i ∈ s → Rel i x✝¹ x✝
rfl