[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]


[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : One α
inst✝ : TopologicalSpace X
f : X → α
⊢ mulTSupport f = ∅ ↔ f = 1
[PROOFSTEP]
rw [mulTSupport, closure_empty_iff, mulSupport_eq_empty_iff]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
⊢ ¬x ∈ mulTSupport f ↔ f =ᶠ[𝓝 x] 1
[PROOFSTEP]
simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop, ←
  disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
⊢ HasCompactMulSupport f ↔ IsCompact (closure (mulSupport f))
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : T2Space α
⊢ (∃ K, IsCompact K ∧ ∀ (x : α), ¬x ∈ K → f x = 1) ↔ HasCompactMulSupport f
[PROOFSTEP]
simp_rw [← nmem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl, hasCompactMulSupport_def,
  exists_compact_superset_iff]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
⊢ IsCompact (range f)
[PROOFSTEP]
cases' range_eq_image_mulTSupport_or f with h2 h2
[GOAL]
case inl
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
h2 : range f = f '' mulTSupport f
⊢ IsCompact (range f)
[PROOFSTEP]
rw [h2]
[GOAL]
case inr
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
h2 : range f = insert 1 (f '' mulTSupport f)
⊢ IsCompact (range f)
[PROOFSTEP]
rw [h2]
[GOAL]
case inl
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
h2 : range f = f '' mulTSupport f
⊢ IsCompact (f '' mulTSupport f)
case inr
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
h2 : range f = insert 1 (f '' mulTSupport f)
⊢ IsCompact (insert 1 (f '' mulTSupport f))
[PROOFSTEP]
exacts [h.image hf, (h.image hf).insert 1]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hg : ∀ {x : β}, g x = 1 ↔ x = 1
⊢ HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f
[PROOFSTEP]
simp_rw [hasCompactMulSupport_def, mulSupport_comp_eq g (@hg) f]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ HasCompactMulSupport (f ∘ g)
[PROOFSTEP]
rw [hasCompactMulSupport_def, Function.mulSupport_comp_eq_preimage]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ IsCompact (closure (g ⁻¹' mulSupport f))
[PROOFSTEP]
refine' isCompact_of_isClosed_subset (hg.isCompact_preimage hf) isClosed_closure _
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ closure (g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f
[PROOFSTEP]
rw [hg.toEmbedding.closure_eq_preimage_closure_image]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ g ⁻¹' closure (g '' (g ⁻¹' mulSupport f)) ⊆ g ⁻¹' mulTSupport f
[PROOFSTEP]
exact preimage_mono (closure_mono <| image_preimage_subset _ _)
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
hf₂ : HasCompactMulSupport f₂
hm : m 1 1 = 1
⊢ HasCompactMulSupport fun x => m (f x) (f₂ x)
[PROOFSTEP]
rw [hasCompactMulSupport_iff_eventuallyEq] at hf hf₂ ⊢
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
⊢ (fun x => m (f x) (f₂ x)) =ᶠ[coclosedCompact α] 1
[PROOFSTEP]
filter_upwards [hf, hf₂] using fun x hx hx₂ => by simp_rw [hx, hx₂, Pi.one_apply, hm]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x✝ : α
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
x : α
hx : f x = OfNat.ofNat 1 x
hx₂ : f₂ x = OfNat.ofNat 1 x
⊢ m (f x) (f₂ x) = OfNat.ofNat 1 x
[PROOFSTEP]
simp_rw [hx, hx₂, Pi.one_apply, hm]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : MonoidWithZero R
inst✝¹ : AddMonoid M
inst✝ : DistribMulAction R M
f : α → R
f' : α → M
x : α
hf : HasCompactSupport f'
⊢ HasCompactSupport (f • f')
[PROOFSTEP]
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : MonoidWithZero R
inst✝¹ : AddMonoid M
inst✝ : DistribMulAction R M
f : α → R
f' : α → M
x : α
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0
[PROOFSTEP]
exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : MonoidWithZero R
inst✝¹ : AddMonoid M
inst✝ : DistribMulAction R M
f : α → R
f' : α → M
x✝ : α
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = OfNat.ofNat 0 x
⊢ (f • f') x = OfNat.ofNat 0 x
[PROOFSTEP]
simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x : α
hf : HasCompactSupport f
⊢ HasCompactSupport (f • f')
[PROOFSTEP]
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x : α
hf : f =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0
[PROOFSTEP]
exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x✝ : α
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = OfNat.ofNat 0 x
⊢ (f • f') x = OfNat.ofNat 0 x
[PROOFSTEP]
simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x : α
hf : HasCompactSupport f'
⊢ HasCompactSupport (f • f')
[PROOFSTEP]
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x : α
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0
[PROOFSTEP]
refine' hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x✝ : α
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = OfNat.ofNat 0 x
⊢ (f • f') x = OfNat.ofNat 0 x
[PROOFSTEP]
simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x : α
hf : HasCompactSupport f
⊢ HasCompactSupport (f * f')
[PROOFSTEP]
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x : α
hf : f =ᶠ[coclosedCompact α] 0
⊢ f * f' =ᶠ[coclosedCompact α] 0
[PROOFSTEP]
refine' hf.mono fun x hx => by simp_rw [Pi.mul_apply, hx, Pi.zero_apply, zero_mul]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x✝ : α
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = OfNat.ofNat 0 x
⊢ (f * f') x = OfNat.ofNat 0 x
[PROOFSTEP]
simp_rw [Pi.mul_apply, hx, Pi.zero_apply, zero_mul]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x : α
hf : HasCompactSupport f'
⊢ HasCompactSupport (f * f')
[PROOFSTEP]
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x : α
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f * f' =ᶠ[coclosedCompact α] 0
[PROOFSTEP]
refine' hf.mono fun x hx => by simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x✝ : α
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = OfNat.ofNat 0 x
⊢ (f * f') x = OfNat.ofNat 0 x
[PROOFSTEP]
simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
⊢ ∃ is n, n ∈ 𝓝 x ∧ n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i ∧ ∀ (z : X), z ∈ n → (mulSupport fun i => f i z) ⊆ ↑is
[PROOFSTEP]
obtain ⟨n, hn, hnf⟩ := hlf x
[GOAL]
case intro.intro
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
⊢ ∃ is n, n ∈ 𝓝 x ∧ n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i ∧ ∀ (z : X), z ∈ n → (mulSupport fun i => f i z) ⊆ ↑is
[PROOFSTEP]
classical
let is := hnf.toFinset.filter fun i => x ∈ U i
let js := hnf.toFinset.filter fun j => x ∉ U j
refine'
  ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn _) _, inter_subset_right _ _,
    fun z hz => _⟩
·
  exact
    (biInter_finset_mem js).mpr fun j hj =>
      IsClosed.compl_mem_nhds (isClosed_mulTSupport _) (Set.not_mem_subset (hso j) (Finset.mem_filter.mp hj).2)
· exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2
· have hzn : z ∈ n := by
    rw [inter_assoc] at hz
    exact mem_of_mem_inter_left hz
  replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
  simp only [Finset.mem_filter, Finite.mem_toFinset, mem_setOf_eq, mem_iInter, and_imp] at hz
  suffices (mulSupport fun i => f i z) ⊆ hnf.toFinset
    by
    refine' hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => _
    specialize hz i ⟨z, ⟨hi, hzn⟩⟩
    contrapose hz
    simp [hz, subset_mulTSupport (f i) hi]
  intro i hi
  simp only [Finite.coe_toFinset, mem_setOf_eq]
  exact ⟨z, ⟨hi, hzn⟩⟩
[GOAL]
case intro.intro
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
⊢ ∃ is n, n ∈ 𝓝 x ∧ n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i ∧ ∀ (z : X), z ∈ n → (mulSupport fun i => f i z) ⊆ ↑is
[PROOFSTEP]
let is := hnf.toFinset.filter fun i => x ∈ U i
[GOAL]
case intro.intro
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
⊢ ∃ is n, n ∈ 𝓝 x ∧ n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i ∧ ∀ (z : X), z ∈ n → (mulSupport fun i => f i z) ⊆ ↑is
[PROOFSTEP]
let js := hnf.toFinset.filter fun j => x ∉ U j
[GOAL]
case intro.intro
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
⊢ ∃ is n, n ∈ 𝓝 x ∧ n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i ∧ ∀ (z : X), z ∈ n → (mulSupport fun i => f i z) ⊆ ↑is
[PROOFSTEP]
refine'
  ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn _) _, inter_subset_right _ _,
    fun z hz => _⟩
[GOAL]
case intro.intro.refine'_1
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
⊢ ⋂ (j : ι) (_ : j ∈ js), (mulTSupport (f j))ᶜ ∈ 𝓝 x
[PROOFSTEP]
exact
  (biInter_finset_mem js).mpr fun j hj =>
    IsClosed.compl_mem_nhds (isClosed_mulTSupport _) (Set.not_mem_subset (hso j) (Finset.mem_filter.mp hj).2)
[GOAL]
case intro.intro.refine'_2
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
⊢ ⋂ (i : ι) (_ : i ∈ is), U i ∈ 𝓝 x
[PROOFSTEP]
exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hz : z ∈ (n ∩ ⋂ (j : ι) (_ : j ∈ js), (mulTSupport (f j))ᶜ) ∩ ⋂ (i : ι) (_ : i ∈ is), U i
⊢ (mulSupport fun i => f i z) ⊆ ↑is
[PROOFSTEP]
have hzn : z ∈ n := by
  rw [inter_assoc] at hz
  exact mem_of_mem_inter_left hz
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hz : z ∈ (n ∩ ⋂ (j : ι) (_ : j ∈ js), (mulTSupport (f j))ᶜ) ∩ ⋂ (i : ι) (_ : i ∈ is), U i
⊢ z ∈ n
[PROOFSTEP]
rw [inter_assoc] at hz
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hz : z ∈ n ∩ ((⋂ (j : ι) (_ : j ∈ js), (mulTSupport (f j))ᶜ) ∩ ⋂ (i : ι) (_ : i ∈ is), U i)
⊢ z ∈ n
[PROOFSTEP]
exact mem_of_mem_inter_left hz
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hz : z ∈ (n ∩ ⋂ (j : ι) (_ : j ∈ js), (mulTSupport (f j))ᶜ) ∩ ⋂ (i : ι) (_ : i ∈ is), U i
hzn : z ∈ n
⊢ (mulSupport fun i => f i z) ⊆ ↑is
[PROOFSTEP]
replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : z ∈ ⋂ (j : ι) (_ : j ∈ js), (mulTSupport (f j))ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑is
[PROOFSTEP]
simp only [Finset.mem_filter, Finite.mem_toFinset, mem_setOf_eq, mem_iInter, and_imp] at hz
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ (mulTSupport (f i))ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑is
[PROOFSTEP]
suffices (mulSupport fun i => f i z) ⊆ hnf.toFinset
  by
  refine' hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => _
  specialize hz i ⟨z, ⟨hi, hzn⟩⟩
  contrapose hz
  simp [hz, subset_mulTSupport (f i) hi]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ (mulTSupport (f i))ᶜ
this : (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
⊢ (mulSupport fun i => f i z) ⊆ ↑is
[PROOFSTEP]
refine' hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => _
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ (mulTSupport (f i))ᶜ
this : (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
i : ι
hi : i ∈ mulSupport fun i => f i z
⊢ x ∈ U i
[PROOFSTEP]
specialize hz i ⟨z, ⟨hi, hzn⟩⟩
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
this : (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
i : ι
hi : i ∈ mulSupport fun i => f i z
hz : ¬x ∈ U i → z ∈ (mulTSupport (f i))ᶜ
⊢ x ∈ U i
[PROOFSTEP]
contrapose hz
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
this : (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
i : ι
hi : i ∈ mulSupport fun i => f i z
hz : ¬x ∈ U i
⊢ ¬(¬x ∈ U i → z ∈ (mulTSupport (f i))ᶜ)
[PROOFSTEP]
simp [hz, subset_mulTSupport (f i) hi]
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ (mulTSupport (f i))ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
[PROOFSTEP]
intro i hi
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ (mulTSupport (f i))ᶜ
i : ι
hi : i ∈ mulSupport fun i => f i z
⊢ i ∈ ↑(Finite.toFinset hnf)
[PROOFSTEP]
simp only [Finite.coe_toFinset, mem_setOf_eq]
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
U : ι → Set X
inst✝¹ : TopologicalSpace X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ (mulTSupport (f i))ᶜ
i : ι
hi : i ∈ mulSupport fun i => f i z
⊢ Set.Nonempty (mulSupport (f i) ∩ n)
[PROOFSTEP]
exact ⟨z, ⟨hi, hzn⟩⟩