α : Type u_1
β : Type ?u.7918
σ : Type ?u.7921
τ : Type ?u.7924
T : TopologicalSpace α
F : Realizer α
this : TopologicalSpace.IsTopologicalBasis (range F.F.f)
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)
α : Type u_1
β : Type ?u.7918
σ : Type ?u.7921
τ : Type ?u.7924
T : TopologicalSpace α
F : Realizer α
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)
have := toTopsp_isTopologicalBasis F.F
no goals
α : Type u_1
β : Type ?u.7918
σ : Type ?u.7921
τ : Type ?u.7924
T : TopologicalSpace α
F : Realizer α
this : TopologicalSpace.IsTopologicalBasis (range F.F.f)
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)
rwa [F.eq] at this