α : Type u
β : Type v
γ : Type ?u.52987
δ : Type ?u.52990
ε : Type ?u.52993
ζ : Type ?u.52996
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
x : α × β
s : Set α
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.snd}] x)
⊢ s ∈ 𝓝 x.fst
α : Type u
β : Type v
γ : Type ?u.52987
δ : Type ?u.52990
ε : Type ?u.52993
ζ : Type ?u.52996
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
x : α × β
⊢ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.snd}] x) = 𝓝 x.fst
refine' le_antisymm (continuousAt_fst.mono_left inf_le_left) fun s hs => _
case mk
α : Type u
β : Type v
γ : Type ?u.52987
δ : Type ?u.52990
ε : Type ?u.52993
ζ : Type ?u.52996
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
x : α
y : β
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {(x, y).snd}] (x, y))
⊢ s ∈ 𝓝 (x, y).fst
α : Type u
β : Type v
γ : Type ?u.52987
δ : Type ?u.52990
ε : Type ?u.52993
ζ : Type ?u.52996
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
x : α × β
s : Set α
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.snd}] x)
⊢ s ∈ 𝓝 x.fst
rcases x with ⟨x, y⟩
case mk
α : Type u
β : Type v
γ : Type ?u.52987
δ : Type ?u.52990
ε : Type ?u.52993
ζ : Type ?u.52996
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
x : α
y : β
hs : ∃ u, u ∈ 𝓝 x ∧ ∃ v, v ∈ 𝓝 y ∧ u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.snd ⁻¹' {(x, y).snd} → x_1 ∈ Prod.fst ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).fst
case mk
α : Type u
β : Type v
γ : Type ?u.52987
δ : Type ?u.52990
ε : Type ?u.52993
ζ : Type ?u.52996
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
x : α
y : β
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {(x, y).snd}] (x, y))
⊢ s ∈ 𝓝 (x, y).fst
rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs
case mk.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.52987
δ : Type ?u.52990
ε : Type ?u.52993
ζ : Type ?u.52996
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
x : α
y : β
u : Set α
hu : u ∈ 𝓝 x
v : Set β
hv : v ∈ 𝓝 y
H : u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.snd ⁻¹' {(x, y).snd} → x_1 ∈ Prod.fst ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).fst
case mk
α : Type u
β : Type v
γ : Type ?u.52987
δ : Type ?u.52990
ε : Type ?u.52993
ζ : Type ?u.52996
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
x : α
y : β
hs : ∃ u, u ∈ 𝓝 x ∧ ∃ v, v ∈ 𝓝 y ∧ u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.snd ⁻¹' {(x, y).snd} → x_1 ∈ Prod.fst ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).fst
rcases hs with ⟨u, hu, v, hv, H⟩
case mk.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.52987
δ : Type ?u.52990
ε : Type ?u.52993
ζ : Type ?u.52996
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
x : α
y : β
u : Set α
hu : u ∈ 𝓝 x
v : Set β
hv : v ∈ 𝓝 y
H : ∀ (x : α), x ∈ u → ∀ (y_1 : β), y_1 ∈ v → y_1 = y → x ∈ s
⊢ s ∈ 𝓝 (x, y).fst
case mk.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.52987
δ : Type ?u.52990
ε : Type ?u.52993
ζ : Type ?u.52996
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
x : α
y : β
u : Set α
hu : u ∈ 𝓝 x
v : Set β
hv : v ∈ 𝓝 y
H : u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.snd ⁻¹' {(x, y).snd} → x_1 ∈ Prod.fst ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).fst
simp only [prod_subset_iff, mem_singleton_iff, mem_setOf_eq, mem_preimage] at H
no goals
case mk.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.52987
δ : Type ?u.52990
ε : Type ?u.52993
ζ : Type ?u.52996
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
x : α
y : β
u : Set α
hu : u ∈ 𝓝 x
v : Set β
hv : v ∈ 𝓝 y
H : ∀ (x : α), x ∈ u → ∀ (y_1 : β), y_1 ∈ v → y_1 = y → x ∈ s
⊢ s ∈ 𝓝 (x, y).fst
exact mem_of_superset hu fun z hz => H _ hz _ (mem_of_mem_nhds hv) rfl