X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : ↑(productOfMemOpens X) x1 = ↑(productOfMemOpens X) x2
⊢ x1 = x2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
⊢ Function.Injective ↑(productOfMemOpens X)
intro x1 x2 h
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : ↑(productOfMemOpens X) x1 = ↑(productOfMemOpens X) x2
⊢ Inseparable x1 x2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : ↑(productOfMemOpens X) x1 = ↑(productOfMemOpens X) x2
⊢ x1 = x2
apply Inseparable.eq
no goals
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : ↑(productOfMemOpens X) x1 = ↑(productOfMemOpens X) x2
⊢ Inseparable x1 x2
rw [← Inducing.inseparable_iff (productOfMemOpens_inducing X), h]