[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
⊢ TFAE
    [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)]
[PROOFSTEP]
tfae_have 1 → 2
[GOAL]
case tfae_1_to_2
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
⊢ x ⤳ y → pure x ≤ 𝓝 y
[PROOFSTEP]
exact (pure_le_nhds _).trans
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
⊢ TFAE
    [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)]
[PROOFSTEP]
tfae_have 2 → 3
[GOAL]
case tfae_2_to_3
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
⊢ pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
[PROOFSTEP]
exact fun h s hso hy => h (hso.mem_nhds hy)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
⊢ TFAE
    [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)]
[PROOFSTEP]
tfae_have 3 → 4
[GOAL]
case tfae_3_to_4
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
⊢ (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
[PROOFSTEP]
exact fun h s hsc hx => of_not_not fun hy => h sᶜ hsc.isOpen_compl hy hx
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
⊢ TFAE
    [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)]
[PROOFSTEP]
tfae_have 4 → 5
[GOAL]
case tfae_4_to_5
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
⊢ (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
[PROOFSTEP]
exact fun h => h _ isClosed_closure (subset_closure <| mem_singleton _)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
⊢ TFAE
    [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)]
[PROOFSTEP]
tfae_have 6 ↔ 5
[GOAL]
case tfae_6_iff_5
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
⊢ closure {y} ⊆ closure {x} ↔ y ∈ closure {x}
[PROOFSTEP]
exact isClosed_closure.closure_subset_iff.trans singleton_subset_iff
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
tfae_6_iff_5 : closure {y} ⊆ closure {x} ↔ y ∈ closure {x}
⊢ TFAE
    [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)]
[PROOFSTEP]
tfae_have 5 ↔ 7
[GOAL]
case tfae_5_iff_7
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
tfae_6_iff_5 : closure {y} ⊆ closure {x} ↔ y ∈ closure {x}
⊢ y ∈ closure {x} ↔ ClusterPt y (pure x)
[PROOFSTEP]
rw [mem_closure_iff_clusterPt, principal_singleton]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
tfae_6_iff_5 : closure {y} ⊆ closure {x} ↔ y ∈ closure {x}
tfae_5_iff_7 : y ∈ closure {x} ↔ ClusterPt y (pure x)
⊢ TFAE
    [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)]
[PROOFSTEP]
tfae_have 5 → 1
[GOAL]
case tfae_5_to_1
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
tfae_6_iff_5 : closure {y} ⊆ closure {x} ↔ y ∈ closure {x}
tfae_5_iff_7 : y ∈ closure {x} ↔ ClusterPt y (pure x)
⊢ y ∈ closure {x} → x ⤳ y
[PROOFSTEP]
refine' fun h => (nhds_basis_opens _).ge_iff.2 _
[GOAL]
case tfae_5_to_1
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
tfae_6_iff_5 : closure {y} ⊆ closure {x} ↔ y ∈ closure {x}
tfae_5_iff_7 : y ∈ closure {x} ↔ ClusterPt y (pure x)
h : y ∈ closure {x}
⊢ ∀ (i' : Set X), y ∈ i' ∧ IsOpen i' → i' ∈ 𝓝 x
[PROOFSTEP]
rintro s ⟨hy, ho⟩
[GOAL]
case tfae_5_to_1.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s✝ : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
tfae_6_iff_5 : closure {y} ⊆ closure {x} ↔ y ∈ closure {x}
tfae_5_iff_7 : y ∈ closure {x} ↔ ClusterPt y (pure x)
h : y ∈ closure {x}
s : Set X
hy : y ∈ s
ho : IsOpen s
⊢ s ∈ 𝓝 x
[PROOFSTEP]
rcases mem_closure_iff.1 h s ho hy with ⟨z, hxs, rfl : z = x⟩
[GOAL]
case tfae_5_to_1.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y✝ z✝ : X
s✝ : Set X
f : X → Y
y : X
s : Set X
hy : y ∈ s
ho : IsOpen s
z : X
hxs : z ∈ s
tfae_1_to_2 : z ⤳ y → pure z ≤ 𝓝 y
tfae_2_to_3 : pure z ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → z ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → z ∈ s) → ∀ (s : Set X), IsClosed s → z ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → z ∈ s → y ∈ s) → y ∈ closure {z}
tfae_6_iff_5 : closure {y} ⊆ closure {z} ↔ y ∈ closure {z}
tfae_5_iff_7 : y ∈ closure {z} ↔ ClusterPt y (pure z)
h : y ∈ closure {z}
⊢ s ∈ 𝓝 z
[PROOFSTEP]
exact ho.mem_nhds hxs
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
tfae_6_iff_5 : closure {y} ⊆ closure {x} ↔ y ∈ closure {x}
tfae_5_iff_7 : y ∈ closure {x} ↔ ClusterPt y (pure x)
tfae_5_to_1 : y ∈ closure {x} → x ⤳ y
⊢ TFAE
    [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)]
[PROOFSTEP]
tfae_finish
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
hf : Inducing f
⊢ f x ⤳ f y ↔ x ⤳ y
[PROOFSTEP]
simp only [specializes_iff_mem_closure, hf.closure_eq_preimage_closure_image, image_singleton, mem_preimage]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
x₁ x₂ : X
y₁ y₂ : Y
⊢ (x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂
[PROOFSTEP]
simp only [Specializes, nhds_prod_eq, prod_le_prod]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f✝ : X → Y
f g : (i : ι) → π i
⊢ f ⤳ g ↔ ∀ (i : ι), f i ⤳ g i
[PROOFSTEP]
simp only [Specializes, nhds_pi, pi_le_pi]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ ¬x ⤳ y ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ ¬x ∈ S
[PROOFSTEP]
rw [specializes_iff_forall_open]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (¬∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ ¬x ∈ S
[PROOFSTEP]
push_neg
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (∃ s, IsOpen s ∧ y ∈ s ∧ ¬x ∈ s) ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ ¬x ∈ S
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ ¬x ⤳ y ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ ¬y ∈ S
[PROOFSTEP]
rw [specializes_iff_forall_closed]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (¬∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ ¬y ∈ S
[PROOFSTEP]
push_neg
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (∃ s, IsClosed s ∧ x ∈ s ∧ ¬y ∈ s) ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ ¬y ∈ S
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (x ~ᵢ y) ↔ ∀ (s : Set X), IsOpen s → (x ∈ s ↔ y ∈ s)
[PROOFSTEP]
simp only [inseparable_iff_specializes_and, specializes_iff_forall_open, ← forall_and, ← iff_def, Iff.comm]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ ¬(x ~ᵢ y) ↔ ∃ s, IsOpen s ∧ Xor' (x ∈ s) (y ∈ s)
[PROOFSTEP]
simp [inseparable_iff_forall_open, ← xor_iff_not_iff]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (x ~ᵢ y) ↔ ∀ (s : Set X), IsClosed s → (x ∈ s ↔ y ∈ s)
[PROOFSTEP]
simp only [inseparable_iff_specializes_and, specializes_iff_forall_closed, ← forall_and, ← iff_def]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ x ⤳ y ∧ y ⤳ x ↔ x ∈ closure {y} ∧ y ∈ closure {x}
[PROOFSTEP]
simp only [specializes_iff_mem_closure, and_comm]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (x ~ᵢ y) ↔ closure {x} = closure {y}
[PROOFSTEP]
simp only [inseparable_iff_specializes_and, specializes_iff_closure_subset, ← subset_antisymm_iff, eq_comm]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
hf : Inducing f
⊢ (f x ~ᵢ f y) ↔ (x ~ᵢ y)
[PROOFSTEP]
simp only [inseparable_iff_specializes_and, hf.specializes_iff]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
x₁ x₂ : X
y₁ y₂ : Y
⊢ ((x₁, y₁) ~ᵢ (x₂, y₂)) ↔ (x₁ ~ᵢ x₂) ∧ (y₁ ~ᵢ y₂)
[PROOFSTEP]
simp only [Inseparable, nhds_prod_eq, prod_inj]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f✝ : X → Y
f g : (i : ι) → π i
⊢ (f ~ᵢ g) ↔ ∀ (i : ι), f i ~ᵢ g i
[PROOFSTEP]
simp only [Inseparable, nhds_pi, funext_iff, pi_inj]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
hs : IsOpen s
⊢ mk ⁻¹' (mk '' s) = s
[PROOFSTEP]
refine' Subset.antisymm _ (subset_preimage_image _ _)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
hs : IsOpen s
⊢ mk ⁻¹' (mk '' s) ⊆ s
[PROOFSTEP]
rintro x ⟨y, hys, hxy⟩
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
hs : IsOpen s
x y : X
hys : y ∈ s
hxy : mk y = mk x
⊢ x ∈ s
[PROOFSTEP]
exact ((mk_eq_mk.1 hxy).mem_open_iff hs).1 hys
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s✝ : Set X
f : X → Y
t : Set (SeparationQuotient X)
s : Set X
hs : IsOpen s
⊢ IsOpen (mk ⁻¹' (mk '' s))
[PROOFSTEP]
rwa [preimage_image_mk_open hs]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
hs : IsClosed s
⊢ mk ⁻¹' (mk '' s) = s
[PROOFSTEP]
refine' Subset.antisymm _ (subset_preimage_image _ _)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
hs : IsClosed s
⊢ mk ⁻¹' (mk '' s) ⊆ s
[PROOFSTEP]
rintro x ⟨y, hys, hxy⟩
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
hs : IsClosed s
x y : X
hys : y ∈ s
hxy : mk y = mk x
⊢ x ∈ s
[PROOFSTEP]
exact ((mk_eq_mk.1 hxy).mem_closed_iff hs).1 hys
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
⊢ IsClosed (Set.range mk)
[PROOFSTEP]
rw [range_mk]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
⊢ IsClosed univ
[PROOFSTEP]
exact isClosed_univ
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
⊢ Filter.map mk (𝓝 x) = 𝓝 (mk x)
[PROOFSTEP]
rw [← comap_mk_nhds_mk, map_comap_of_surjective surjective_mk]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
⊢ Filter.map mk (𝓝ˢ s) = 𝓝ˢ (mk '' s)
[PROOFSTEP]
rw [← comap_mk_nhdsSet_image, map_comap_of_surjective surjective_mk]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
⊢ comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t)
[PROOFSTEP]
conv_lhs => rw [← image_preimage_eq t surjective_mk, comap_mk_nhdsSet_image]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
| comap mk (𝓝ˢ t)
[PROOFSTEP]
rw [← image_preimage_eq t surjective_mk, comap_mk_nhdsSet_image]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
| comap mk (𝓝ˢ t)
[PROOFSTEP]
rw [← image_preimage_eq t surjective_mk, comap_mk_nhdsSet_image]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
| comap mk (𝓝ˢ t)
[PROOFSTEP]
rw [← image_preimage_eq t surjective_mk, comap_mk_nhdsSet_image]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
x : X
y : Y
⊢ Filter.map (Prod.map mk mk) (𝓝 (x, y)) = 𝓝 (mk x, mk y)
[PROOFSTEP]
rw [nhds_prod_eq, ← prod_map_map_eq', map_mk_nhds, map_mk_nhds, nhds_prod_eq]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y z : X
s✝ : Set X
f : X → Y
t s : Set (SeparationQuotient X)
x : X
⊢ Filter.map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x
[PROOFSTEP]
rw [nhdsWithin, ← comap_principal, Filter.push_pull, nhdsWithin, map_mk_nhds]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y z : X
s : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → α
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
x : X
l : Filter α
⊢ Tendsto (lift f hf) (𝓝 (mk x)) l ↔ Tendsto f (𝓝 x) l
[PROOFSTEP]
simp only [← map_mk_nhds, tendsto_map'_iff, lift_comp_mk]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y z : X
s✝ : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → α
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
x : X
s : Set (SeparationQuotient X)
l : Filter α
⊢ Tendsto (lift f hf) (𝓝[s] mk x) l ↔ Tendsto f (𝓝[mk ⁻¹' s] x) l
[PROOFSTEP]
simp only [← map_mk_nhdsWithin_preimage, tendsto_map'_iff, lift_comp_mk]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s✝ : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → Y
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
s : Set (SeparationQuotient X)
⊢ ContinuousOn (lift f hf) s ↔ ContinuousOn f (mk ⁻¹' s)
[PROOFSTEP]
simp only [ContinuousOn, surjective_mk.forall, continuousWithinAt_lift, mem_preimage]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → Y
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
⊢ Continuous (lift f hf) ↔ Continuous f
[PROOFSTEP]
simp only [continuous_iff_continuousOn_univ, continuousOn_lift, preimage_univ]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝 (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l
[PROOFSTEP]
rw [← map_prod_map_mk_nhds, tendsto_map'_iff]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf) ∘ Prod.map mk mk) (𝓝 (x, y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s✝ : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (SeparationQuotient X × SeparationQuotient Y)
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝[s] (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l
[PROOFSTEP]
rw [nhdsWithin, ← map_prod_map_mk_nhds, ← Filter.push_pull, comap_principal]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s✝ : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (SeparationQuotient X × SeparationQuotient Y)
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (Filter.map (Prod.map mk mk) (𝓝 (x, y) ⊓ 𝓟 (Prod.map mk mk ⁻¹' s))) l ↔
    Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s✝ : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (SeparationQuotient X × SeparationQuotient Y)
⊢ ContinuousOn (uncurry (lift₂ f hf)) s ↔ ContinuousOn (uncurry f) (Prod.map mk mk ⁻¹' s)
[PROOFSTEP]
simp_rw [ContinuousOn, (surjective_mk.Prod_map surjective_mk).forall, Prod.forall, Prod.map, continuousWithinAt_lift₂]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s✝ : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (SeparationQuotient X × SeparationQuotient Y)
⊢ (∀ (a : X) (b : Y), (mk a, mk b) ∈ s → ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (a, b)) ↔
    ∀ (a : X) (b : Y),
      (a, b) ∈ (fun x => (mk x.fst, mk x.snd)) ⁻¹' s →
        ContinuousWithinAt (uncurry f) ((fun x => (mk x.fst, mk x.snd)) ⁻¹' s) (a, b)
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
π : ι → Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
⊢ Continuous (uncurry (lift₂ f hf)) ↔ Continuous (uncurry f)
[PROOFSTEP]
simp only [continuous_iff_continuousOn_univ, continuousOn_lift₂, preimage_univ]
