Lean4
instance : InfSet (Pretopology C) where
sInf
T :=
{ coverings := sInf ((fun J ↦ J.coverings) '' T)
has_isos := fun X Y f _ ↦
by
simp only [sInf_apply, Set.iInf_eq_iInter, Set.iInter_coe_set, Set.mem_image, Set.iInter_exists,
Set.biInter_and', Set.iInter_iInter_eq_right, Set.mem_iInter]
intro t _
exact t.has_isos f
pullbacks := fun X Y f S hS ↦
by
simp only [sInf_apply, Set.iInf_eq_iInter, Set.iInter_coe_set, Set.mem_image, Set.iInter_exists,
Set.biInter_and', Set.iInter_iInter_eq_right, Set.mem_iInter] at hS ⊢
intro t ht
exact t.pullbacks f S (hS t ht)
transitive := fun X S Ti hS hTi ↦
by
simp only [sInf_apply, Set.iInf_eq_iInter, Set.iInter_coe_set, Set.mem_image, Set.iInter_exists,
Set.biInter_and', Set.iInter_iInter_eq_right, Set.mem_iInter] at hS hTi ⊢
intro t ht
exact t.transitive S Ti (hS t ht) (fun Y f H ↦ hTi f H t ht) }
