R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ TopologicalSpace.IsTopologicalBasis (SetLike.coe '' Set.range basicOpen)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ TopologicalSpace.Opens.IsBasis (Set.range basicOpen)
unfold TopologicalSpace.Opens.IsBasis
case h.e'_3
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ SetLike.coe '' Set.range basicOpen = Set.range fun r => ↑(basicOpen r)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ TopologicalSpace.IsTopologicalBasis (SetLike.coe '' Set.range basicOpen)
convert isTopologicalBasis_basic_opens (R := R)
case h.e'_3
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ Set.range (SetLike.coe ∘ basicOpen) = Set.range fun r => ↑(basicOpen r)
case h.e'_3
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ SetLike.coe '' Set.range basicOpen = Set.range fun r => ↑(basicOpen r)
rw [← Set.range_comp]
no goals
case h.e'_3
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ Set.range (SetLike.coe ∘ basicOpen) = Set.range fun r => ↑(basicOpen r)
rfl