[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
hα : DiscreteTopology α
hβ : DiscreteTopology β
⊢ coinduced inl inst✝¹ = ⊥ ∧ coinduced inr inst✝ = ⊥
[PROOFSTEP]
simp [hα.eq_bot, hβ.eq_bot]
[GOAL]
α : Type u
β✝ : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
β : α → Type v
inst✝ : (a : α) → TopologicalSpace (β a)
h : ∀ (a : α), DiscreteTopology (β a)
x✝ : α
⊢ coinduced (mk x✝) ((fun a => inst✝ a) x✝) = ⊥
[PROOFSTEP]
simp only [(h _).eq_bot, coinduced_bot]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝ : TopologicalSpace α
s t : Set α
x : ↑s
⊢ 𝓝[Subtype.val ⁻¹' t] x = ⊥ ↔ 𝓝[t] ↑x ⊓ 𝓟 s = ⊥
[PROOFSTEP]
rw [inf_principal_eq_bot_iff_comap, nhdsWithin, nhdsWithin, comap_inf, comap_principal, nhds_induced]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝ : TopologicalSpace α
S : Set α
x : ↑S
⊢ 𝓝[{x}ᶜ] x = ⊥ ↔ 𝓝[{↑x}ᶜ] ↑x ⊓ 𝓟 S = ⊥
[PROOFSTEP]
rw [← nhdsWithin_subtype_eq_bot_iff, preimage_compl, ← image_singleton, Subtype.coe_injective.preimage_image]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝ : TopologicalSpace α
S : Set α
x : ↑S
⊢ NeBot (𝓝[{x}ᶜ] x) ↔ NeBot (𝓝[{↑x}ᶜ] ↑x ⊓ 𝓟 S)
[PROOFSTEP]
rw [neBot_iff, neBot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝ : TopologicalSpace α
S : Set α
⊢ DiscreteTopology ↑S ↔ ∀ (x : α), x ∈ S → 𝓝[{x}ᶜ] x ⊓ 𝓟 S = ⊥
[PROOFSTEP]
simp_rw [discreteTopology_iff_nhds_ne, SetCoe.forall', nhds_ne_subtype_eq_bot_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
⊢ (fun s => Set.Nonempty s → Set.Finite sᶜ) univ
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
s t : Set (CofiniteTopology α)
⊢ (fun s => Set.Nonempty s → Set.Finite sᶜ) s →
    (fun s => Set.Nonempty s → Set.Finite sᶜ) t → (fun s => Set.Nonempty s → Set.Finite sᶜ) (s ∩ t)
[PROOFSTEP]
rintro hs ht ⟨x, hxs, hxt⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
s t : Set (CofiniteTopology α)
hs : Set.Nonempty s → Set.Finite sᶜ
ht : Set.Nonempty t → Set.Finite tᶜ
x : CofiniteTopology α
hxs : x ∈ s
hxt : x ∈ t
⊢ Set.Finite (s ∩ t)ᶜ
[PROOFSTEP]
rw [compl_inter]
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
s t : Set (CofiniteTopology α)
hs : Set.Nonempty s → Set.Finite sᶜ
ht : Set.Nonempty t → Set.Finite tᶜ
x : CofiniteTopology α
hxs : x ∈ s
hxt : x ∈ t
⊢ Set.Finite (sᶜ ∪ tᶜ)
[PROOFSTEP]
exact (hs ⟨x, hxs⟩).union (ht ⟨x, hxt⟩)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
⊢ ∀ (s : Set (Set (CofiniteTopology α))),
    (∀ (t : Set (CofiniteTopology α)), t ∈ s → (fun s => Set.Nonempty s → Set.Finite sᶜ) t) →
      (fun s => Set.Nonempty s → Set.Finite sᶜ) (⋃₀ s)
[PROOFSTEP]
rintro s h ⟨x, t, hts, hzt⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
s : Set (Set (CofiniteTopology α))
h : ∀ (t : Set (CofiniteTopology α)), t ∈ s → (fun s => Set.Nonempty s → Set.Finite sᶜ) t
x : CofiniteTopology α
t : Set (CofiniteTopology α)
hts : t ∈ s
hzt : x ∈ t
⊢ Set.Finite (⋃₀ s)ᶜ
[PROOFSTEP]
rw [Set.compl_sUnion]
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
s : Set (Set (CofiniteTopology α))
h : ∀ (t : Set (CofiniteTopology α)), t ∈ s → (fun s => Set.Nonempty s → Set.Finite sᶜ) t
x : CofiniteTopology α
t : Set (CofiniteTopology α)
hts : t ∈ s
hzt : x ∈ t
⊢ Set.Finite (⋂₀ (compl '' s))
[PROOFSTEP]
exact Set.Finite.sInter (mem_image_of_mem _ hts) (h t hts ⟨x, hzt⟩)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
s : Set (CofiniteTopology α)
⊢ IsOpen s ↔ s = ∅ ∨ Set.Finite sᶜ
[PROOFSTEP]
simp only [isOpen_iff, nonempty_iff_ne_empty, or_iff_not_imp_left]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
s : Set (CofiniteTopology α)
⊢ IsClosed s ↔ s = univ ∨ Set.Finite s
[PROOFSTEP]
simp only [← isOpen_compl_iff, isOpen_iff', compl_compl, compl_empty_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
a : CofiniteTopology α
⊢ 𝓝 a = pure a ⊔ cofinite
[PROOFSTEP]
ext U
[GOAL]
case a
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
a : CofiniteTopology α
U : Set (CofiniteTopology α)
⊢ U ∈ 𝓝 a ↔ U ∈ pure a ⊔ cofinite
[PROOFSTEP]
rw [mem_nhds_iff]
[GOAL]
case a
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
a : CofiniteTopology α
U : Set (CofiniteTopology α)
⊢ (∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t) ↔ U ∈ pure a ⊔ cofinite
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
a : CofiniteTopology α
U : Set (CofiniteTopology α)
⊢ (∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t) → U ∈ pure a ⊔ cofinite
[PROOFSTEP]
rintro ⟨V, hVU, V_op, haV⟩
[GOAL]
case a.mp.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
a : CofiniteTopology α
U V : Set (CofiniteTopology α)
hVU : V ⊆ U
V_op : IsOpen V
haV : a ∈ V
⊢ U ∈ pure a ⊔ cofinite
[PROOFSTEP]
exact mem_sup.mpr ⟨hVU haV, mem_of_superset (V_op ⟨_, haV⟩) hVU⟩
[GOAL]
case a.mpr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
a : CofiniteTopology α
U : Set (CofiniteTopology α)
⊢ U ∈ pure a ⊔ cofinite → ∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t
[PROOFSTEP]
rintro ⟨hU : a ∈ U, hU' : Uᶜ.Finite⟩
[GOAL]
case a.mpr.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
a : CofiniteTopology α
U : Set (CofiniteTopology α)
hU : a ∈ U
hU' : Set.Finite Uᶜ
⊢ ∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t
[PROOFSTEP]
exact ⟨U, Subset.rfl, fun _ => hU', hU⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
a : CofiniteTopology α
s : Set (CofiniteTopology α)
⊢ s ∈ 𝓝 a ↔ a ∈ s ∧ Set.Finite sᶜ
[PROOFSTEP]
simp [nhds_eq]
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.27593
β : Type ?u.27599
γ : Type ?u.27605
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
⊢ Sort ?u.27607
[PROOFSTEP]
haveI := ta1
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.27593
β : Type ?u.27599
γ : Type ?u.27605
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
this : TopologicalSpace α
⊢ Sort ?u.27607
[PROOFSTEP]
haveI := tb1
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.27593
β : Type ?u.27599
γ : Type ?u.27605
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
this✝ : TopologicalSpace α
this : TopologicalSpace β
⊢ Sort ?u.27607
[PROOFSTEP]
exact Continuous fun p : α × β => f p.1 p.2
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.27593
β : Type ?u.27599
γ : Type ?u.27605
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
⊢ Sort ?u.27610
[PROOFSTEP]
haveI := ta1 ⊓ ta2
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.27593
β : Type ?u.27599
γ : Type ?u.27605
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
this : TopologicalSpace α
⊢ Sort ?u.27610
[PROOFSTEP]
haveI := tb1 ⊓ tb2
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.27593
β : Type ?u.27599
γ : Type ?u.27605
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
this✝ : TopologicalSpace α
this : TopologicalSpace β
⊢ Sort ?u.27610
[PROOFSTEP]
exact Continuous fun p : α × β => f p.1 p.2
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
⊢ Continuous fun p => f p.fst p.snd
[PROOFSTEP]
have ha := @continuous_inf_dom_left _ _ id ta1 ta2 ta1 (@continuous_id _ (id _))
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
ha : Continuous id
⊢ Continuous fun p => f p.fst p.snd
[PROOFSTEP]
have hb := @continuous_inf_dom_left _ _ id tb1 tb2 tb1 (@continuous_id _ (id _))
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
ha : Continuous id
hb : Continuous id
⊢ Continuous fun p => f p.fst p.snd
[PROOFSTEP]
have h_continuous_id := @Continuous.prod_map _ _ _ _ ta1 tb1 (ta1 ⊓ ta2) (tb1 ⊓ tb2) _ _ ha hb
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
ha : Continuous id
hb : Continuous id
h_continuous_id : Continuous fun x => (id x.fst, id x.snd)
⊢ Continuous fun p => f p.fst p.snd
[PROOFSTEP]
exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ h h_continuous_id
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.28286
β : Type ?u.28292
γ : Type ?u.28298
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
⊢ Sort ?u.28300
[PROOFSTEP]
haveI := ta2
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.28286
β : Type ?u.28292
γ : Type ?u.28298
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
this : TopologicalSpace α
⊢ Sort ?u.28300
[PROOFSTEP]
haveI := tb2
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.28286
β : Type ?u.28292
γ : Type ?u.28298
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
this✝ : TopologicalSpace α
this : TopologicalSpace β
⊢ Sort ?u.28300
[PROOFSTEP]
exact Continuous fun p : α × β => f p.1 p.2
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.28286
β : Type ?u.28292
γ : Type ?u.28298
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
⊢ Sort ?u.28303
[PROOFSTEP]
haveI := ta1 ⊓ ta2
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.28286
β : Type ?u.28292
γ : Type ?u.28298
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
this : TopologicalSpace α
⊢ Sort ?u.28303
[PROOFSTEP]
haveI := tb1 ⊓ tb2
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.28286
β : Type ?u.28292
γ : Type ?u.28298
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
this✝ : TopologicalSpace α
this : TopologicalSpace β
⊢ Sort ?u.28303
[PROOFSTEP]
exact Continuous fun p : α × β => f p.1 p.2
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
⊢ Continuous fun p => f p.fst p.snd
[PROOFSTEP]
have ha := @continuous_inf_dom_right _ _ id ta1 ta2 ta2 (@continuous_id _ (id _))
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
ha : Continuous id
⊢ Continuous fun p => f p.fst p.snd
[PROOFSTEP]
have hb := @continuous_inf_dom_right _ _ id tb1 tb2 tb2 (@continuous_id _ (id _))
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
ha : Continuous id
hb : Continuous id
⊢ Continuous fun p => f p.fst p.snd
[PROOFSTEP]
have h_continuous_id := @Continuous.prod_map _ _ _ _ ta2 tb2 (ta1 ⊓ ta2) (tb1 ⊓ tb2) _ _ ha hb
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
ta1 ta2 : TopologicalSpace α
tb1 tb2 : TopologicalSpace β
tc1 : TopologicalSpace γ
h : Continuous fun p => f p.fst p.snd
ha : Continuous id
hb : Continuous id
h_continuous_id : Continuous fun x => (id x.fst, id x.snd)
⊢ Continuous fun p => f p.fst p.snd
[PROOFSTEP]
exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ h h_continuous_id
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.28980
β : Type ?u.28984
γ : Type ?u.28993
f : α → β → γ
tas : Set (TopologicalSpace α)
tbs : Set (TopologicalSpace β)
ta : TopologicalSpace α
tb : TopologicalSpace β
tc : TopologicalSpace γ
ha : ta ∈ tas
hb : tb ∈ tbs
hf : Continuous fun p => f p.fst p.snd
⊢ Sort ?u.29158
[PROOFSTEP]
haveI := sInf tas
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.28980
β : Type ?u.28984
γ : Type ?u.28993
f : α → β → γ
tas : Set (TopologicalSpace α)
tbs : Set (TopologicalSpace β)
ta : TopologicalSpace α
tb : TopologicalSpace β
tc : TopologicalSpace γ
ha : ta ∈ tas
hb : tb ∈ tbs
hf : Continuous fun p => f p.fst p.snd
this : TopologicalSpace α
⊢ Sort ?u.29158
[PROOFSTEP]
haveI := sInf tbs
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type ?u.28980
β : Type ?u.28984
γ : Type ?u.28993
f : α → β → γ
tas : Set (TopologicalSpace α)
tbs : Set (TopologicalSpace β)
ta : TopologicalSpace α
tb : TopologicalSpace β
tc : TopologicalSpace γ
ha : ta ∈ tas
hb : tb ∈ tbs
hf : Continuous fun p => f p.fst p.snd
this✝ : TopologicalSpace α
this : TopologicalSpace β
⊢ Sort ?u.29158
[PROOFSTEP]
exact @Continuous _ _ _ tc fun p : α × β => f p.1 p.2
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
tas : Set (TopologicalSpace α)
tbs : Set (TopologicalSpace β)
ta : TopologicalSpace α
tb : TopologicalSpace β
tc : TopologicalSpace γ
ha : ta ∈ tas
hb : tb ∈ tbs
hf : Continuous fun p => f p.fst p.snd
⊢ Continuous fun p => f p.fst p.snd
[PROOFSTEP]
have ha := continuous_sInf_dom ha continuous_id
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
tas : Set (TopologicalSpace α)
tbs : Set (TopologicalSpace β)
ta : TopologicalSpace α
tb : TopologicalSpace β
tc : TopologicalSpace γ
ha✝ : ta ∈ tas
hb : tb ∈ tbs
hf : Continuous fun p => f p.fst p.snd
ha : Continuous id
⊢ Continuous fun p => f p.fst p.snd
[PROOFSTEP]
have hb := continuous_sInf_dom hb continuous_id
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
tas : Set (TopologicalSpace α)
tbs : Set (TopologicalSpace β)
ta : TopologicalSpace α
tb : TopologicalSpace β
tc : TopologicalSpace γ
ha✝ : ta ∈ tas
hb✝ : tb ∈ tbs
hf : Continuous fun p => f p.fst p.snd
ha : Continuous id
hb : Continuous id
⊢ Continuous fun p => f p.fst p.snd
[PROOFSTEP]
have h_continuous_id := @Continuous.prod_map _ _ _ _ ta tb (sInf tas) (sInf tbs) _ _ ha hb
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
tas : Set (TopologicalSpace α)
tbs : Set (TopologicalSpace β)
ta : TopologicalSpace α
tb : TopologicalSpace β
tc : TopologicalSpace γ
ha✝ : ta ∈ tas
hb✝ : tb ∈ tbs
hf : Continuous fun p => f p.fst p.snd
ha : Continuous id
hb : Continuous id
h_continuous_id : Continuous fun x => (id x.fst, id x.snd)
⊢ Continuous fun p => f p.fst p.snd
[PROOFSTEP]
exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ hf h_continuous_id
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
⊢ 𝓝 (a, b) = 𝓝 a ×ˢ 𝓝 b
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
⊢ 𝓝 (a, b) = Filter.prod (𝓝 a) (𝓝 b)
[PROOFSTEP]
rw [Filter.prod, instTopologicalSpaceProd,
  nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _) (t₂ := TopologicalSpace.induced Prod.snd _), nhds_induced,
  nhds_induced]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
s : Set α
t : Set β
⊢ 𝓝[s ×ˢ t] (a, b) = 𝓝[s] a ×ˢ 𝓝[t] b
[PROOFSTEP]
simp only [nhdsWithin, nhds_prod_eq, ← prod_inf_prod, prod_principal_principal]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
⊢ Continuous (uncurry f)
[PROOFSTEP]
apply continuous_iff_continuousAt.2
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
⊢ ∀ (x : α × β), ContinuousAt (uncurry f) x
[PROOFSTEP]
rintro ⟨a, x⟩
[GOAL]
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
a : α
x : β
⊢ ContinuousAt (uncurry f) (a, x)
[PROOFSTEP]
change map _ _ ≤ _
[GOAL]
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
a : α
x : β
⊢ map (uncurry f) (𝓝 (a, x)) ≤ 𝓝 (uncurry f (a, x))
[PROOFSTEP]
rw [nhds_prod_eq, nhds_discrete, Filter.map_pure_prod]
[GOAL]
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
a : α
x : β
⊢ map (f a) (𝓝 x) ≤ 𝓝 (uncurry f (a, x))
[PROOFSTEP]
exact (hf a).continuousAt
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
s : Set (α × β)
⊢ s ∈ 𝓝 (a, b) ↔ ∃ u, u ∈ 𝓝 a ∧ ∃ v, v ∈ 𝓝 b ∧ u ×ˢ v ⊆ s
[PROOFSTEP]
rw [nhds_prod_eq, mem_prod_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
ιa : Type u_5
ιb : Type u_6
pa : ιa → Prop
pb : ιb → Prop
sa : ιa → Set α
sb : ιb → Set β
a : α
b : β
ha : HasBasis (𝓝 a) pa sa
hb : HasBasis (𝓝 b) pb sb
⊢ HasBasis (𝓝 (a, b)) (fun i => pa i.fst ∧ pb i.snd) fun i => sa i.fst ×ˢ sb i.snd
[PROOFSTEP]
rw [nhds_prod_eq]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
ιa : Type u_5
ιb : Type u_6
pa : ιa → Prop
pb : ιb → Prop
sa : ιa → Set α
sb : ιb → Set β
a : α
b : β
ha : HasBasis (𝓝 a) pa sa
hb : HasBasis (𝓝 b) pb sb
⊢ HasBasis (𝓝 a ×ˢ 𝓝 b) (fun i => pa i.fst ∧ pb i.snd) fun i => sa i.fst ×ˢ sb i.snd
[PROOFSTEP]
exact ha.prod hb
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
s : Set (α × β)
⊢ (∃ i, ((a ∈ i.fst ∧ IsOpen i.fst) ∧ b ∈ i.snd ∧ IsOpen i.snd) ∧ i.fst ×ˢ i.snd ⊆ s) ↔
    ∃ u v, IsOpen u ∧ a ∈ u ∧ IsOpen v ∧ b ∈ v ∧ u ×ˢ v ⊆ s
[PROOFSTEP]
simp only [Prod.exists, and_comm, and_assoc, and_left_comm]
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
seq : α → β × γ
f : Filter α
x : β × γ
⊢ Tendsto seq f (𝓝 x) ↔ Tendsto (fun n => (seq n).fst) f (𝓝 x.fst) ∧ Tendsto (fun n => (seq n).snd) f (𝓝 x.snd)
[PROOFSTEP]
rw [nhds_prod_eq, Filter.tendsto_prod_iff']
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : DiscreteTopology α
inst✝ : DiscreteTopology β
x✝ : α × β
a : α
b : β
⊢ 𝓝 (a, b) = pure (a, b)
[PROOFSTEP]
rw [nhds_prod_eq, nhds_discrete α, nhds_discrete β, prod_pure_pure]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
a : α
b : β
⊢ s ×ˢ t ∈ 𝓝 (a, b) ↔ s ∈ 𝓝 a ∧ t ∈ 𝓝 b
[PROOFSTEP]
rw [nhds_prod_eq, prod_mem_prod_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
⊢ 𝓝 (a, b) = map Prod.swap (𝓝 (b, a))
[PROOFSTEP]
rw [nhds_prod_eq, Filter.prod_comm, nhds_prod_eq]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
⊢ map (fun p => (p.snd, p.fst)) (𝓝 b ×ˢ 𝓝 a) = map Prod.swap (𝓝 b ×ˢ 𝓝 a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
γ : Type u_5
a : α
b : β
f : Filter γ
ma : γ → α
mb : γ → β
ha : Tendsto ma f (𝓝 a)
hb : Tendsto mb f (𝓝 b)
⊢ Tendsto (fun c => (ma c, mb c)) f (𝓝 (a, b))
[PROOFSTEP]
rw [nhds_prod_eq]
[GOAL]
α : Type u
β : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ✝
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
γ : Type u_5
a : α
b : β
f : Filter γ
ma : γ → α
mb : γ → β
ha : Tendsto ma f (𝓝 a)
hb : Tendsto mb f (𝓝 b)
⊢ Tendsto (fun c => (ma c, mb c)) f (𝓝 a ×ˢ 𝓝 b)
[PROOFSTEP]
exact Filter.Tendsto.prod_mk ha hb
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
p : α × β → Prop
x : α
y : β
h : ∀ᶠ (x : α × β) in 𝓝 (x, y), p x
⊢ ∀ᶠ (x' : α) in 𝓝 x, ∀ᶠ (y' : β) in 𝓝 y, p (x', y')
[PROOFSTEP]
rw [nhds_prod_eq] at h 
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
p : α × β → Prop
x : α
y : β
h : ∀ᶠ (x : α × β) in 𝓝 x ×ˢ 𝓝 y, p x
⊢ ∀ᶠ (x' : α) in 𝓝 x, ∀ᶠ (y' : β) in 𝓝 y, p (x', y')
[PROOFSTEP]
exact h.curry
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
s : Set (Set α)
t : Set (Set β)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (α × β) := generateFrom {g | ∃ u, u ∈ s ∧ ∃ v, v ∈ t ∧ g = u ×ˢ v}
u : Set α
hu : u ∈ s
⊢ ⋃ (v : Set β) (_ : v ∈ t), u ×ˢ v = Prod.fst ⁻¹' u
[PROOFSTEP]
simp_rw [← prod_iUnion, ← sUnion_eq_biUnion, ht, prod_univ]
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
s : Set (Set α)
t : Set (Set β)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (α × β) := generateFrom {g | ∃ u, u ∈ s ∧ ∃ v, v ∈ t ∧ g = u ×ˢ v}
u : Set α
hu : u ∈ s
this : ⋃ (v : Set β) (_ : v ∈ t), u ×ˢ v = Prod.fst ⁻¹' u
⊢ TopologicalSpace.IsOpen (Prod.fst ⁻¹' u)
[PROOFSTEP]
rw [← this]
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
s : Set (Set α)
t : Set (Set β)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (α × β) := generateFrom {g | ∃ u, u ∈ s ∧ ∃ v, v ∈ t ∧ g = u ×ˢ v}
u : Set α
hu : u ∈ s
this : ⋃ (v : Set β) (_ : v ∈ t), u ×ˢ v = Prod.fst ⁻¹' u
⊢ TopologicalSpace.IsOpen (⋃ (v : Set β) (_ : v ∈ t), u ×ˢ v)
[PROOFSTEP]
exact isOpen_iUnion fun v => isOpen_iUnion fun hv => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
s : Set (Set α)
t : Set (Set β)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (α × β) := generateFrom {g | ∃ u, u ∈ s ∧ ∃ v, v ∈ t ∧ g = u ×ˢ v}
v : Set β
hv : v ∈ t
⊢ ⋃ (u : Set α) (_ : u ∈ s), u ×ˢ v = Prod.snd ⁻¹' v
[PROOFSTEP]
simp_rw [← iUnion_prod_const, ← sUnion_eq_biUnion, hs, univ_prod]
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
s : Set (Set α)
t : Set (Set β)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (α × β) := generateFrom {g | ∃ u, u ∈ s ∧ ∃ v, v ∈ t ∧ g = u ×ˢ v}
v : Set β
hv : v ∈ t
this : ⋃ (u : Set α) (_ : u ∈ s), u ×ˢ v = Prod.snd ⁻¹' v
⊢ TopologicalSpace.IsOpen (Prod.snd ⁻¹' v)
[PROOFSTEP]
rw [← this]
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_5
β : Type u_6
s : Set (Set α)
t : Set (Set β)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (α × β) := generateFrom {g | ∃ u, u ∈ s ∧ ∃ v, v ∈ t ∧ g = u ×ˢ v}
v : Set β
hv : v ∈ t
this : ⋃ (u : Set α) (_ : u ∈ s), u ×ˢ v = Prod.snd ⁻¹' v
⊢ TopologicalSpace.IsOpen (⋃ (u : Set α) (_ : u ∈ s), u ×ˢ v)
[PROOFSTEP]
exact isOpen_iUnion fun u => isOpen_iUnion fun hu => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
t : Set α
ht : t ∈ fun s' => inst✝⁵.1 s'
⊢ IsOpen t ∧ IsOpen univ ∧ Prod.fst ⁻¹' t = t ×ˢ univ
[PROOFSTEP]
simpa [Set.prod_eq] using ht
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
t : Set β
ht : t ∈ fun s' => inst✝⁴.1 s'
⊢ IsOpen univ ∧ IsOpen t ∧ Prod.snd ⁻¹' t = univ ×ˢ t
[PROOFSTEP]
simpa [Set.prod_eq] using ht
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set (α × β)
⊢ (∀ (a : α × β), a ∈ s → s ∈ 𝓝 a) ↔
    ∀ (a : α) (b : β), (a, b) ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s
[PROOFSTEP]
simp_rw [Prod.forall, mem_nhds_prod_iff', and_left_comm]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
⊢ instTopologicalSpaceProd = induced (fun p => (f p.fst, g p.snd)) instTopologicalSpaceProd
[PROOFSTEP]
delta instTopologicalSpaceProd
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
⊢ induced Prod.fst (induced f inst✝⁴) ⊓ induced Prod.snd (induced g inst✝²) =
    induced (fun p => (f p.fst, g p.snd)) (induced Prod.fst inst✝⁴ ⊓ induced Prod.snd inst✝²)
[PROOFSTEP]
simp_rw [induced_inf, induced_compose]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
⊢ induced (f ∘ Prod.fst) inst✝⁴ ⊓ induced (g ∘ Prod.snd) inst✝² =
    induced (Prod.fst ∘ fun p => (f p.fst, g p.snd)) inst✝⁴ ⊓ induced (Prod.snd ∘ fun p => (f p.fst, g p.snd)) inst✝²
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
h : ∀ (a : α), Continuous (f a)
x✝ : α × β
a : α
b : β
⊢ ContinuousAt (uncurry f) (a, b)
[PROOFSTEP]
simp only [ContinuousAt, nhds_prod_eq, nhds_discrete α, pure_prod, tendsto_map'_iff, (· ∘ ·), uncurry, (h a).tendsto]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set (α × α)
x : α
hx : s ∈ 𝓝 (x, x)
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s
[PROOFSTEP]
simpa [nhds_prod_eq, (nhds_basis_opens x).prod_self.mem_iff, and_assoc, and_left_comm] using hx
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
x : α × β
⊢ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.snd}] x) = 𝓝 x.fst
[PROOFSTEP]
refine' le_antisymm (continuousAt_fst.mono_left inf_le_left) fun s hs => _
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
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
[PROOFSTEP]
rcases x with ⟨x, y⟩
[GOAL]
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
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
[PROOFSTEP]
rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs 
[GOAL]
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
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
[PROOFSTEP]
rcases hs with ⟨u, hu, v, hv, H⟩
[GOAL]
case mk.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
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
[PROOFSTEP]
simp only [prod_subset_iff, mem_singleton_iff, mem_setOf_eq, mem_preimage] at H 
[GOAL]
case mk.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
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
[PROOFSTEP]
exact mem_of_superset hu fun z hz => H _ hz _ (mem_of_mem_nhds hv) rfl
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
x : α × β
⊢ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.fst}] x) = 𝓝 x.snd
[PROOFSTEP]
refine' le_antisymm (continuousAt_snd.mono_left inf_le_left) fun s hs => _
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
x : α × β
s : Set β
hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.fst}] x)
⊢ s ∈ 𝓝 x.snd
[PROOFSTEP]
rcases x with ⟨x, y⟩
[GOAL]
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set β
x : α
y : β
hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {(x, y).fst}] (x, y))
⊢ s ∈ 𝓝 (x, y).snd
[PROOFSTEP]
rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs 
[GOAL]
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
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.fst ⁻¹' {(x, y).fst} → x_1 ∈ Prod.snd ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).snd
[PROOFSTEP]
rcases hs with ⟨u, hu, v, hv, H⟩
[GOAL]
case mk.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
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.fst ⁻¹' {(x, y).fst} → x_1 ∈ Prod.snd ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).snd
[PROOFSTEP]
simp only [prod_subset_iff, mem_singleton_iff, mem_setOf_eq, mem_preimage] at H 
[GOAL]
case mk.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
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_1 : α), x_1 ∈ u → ∀ (y : β), y ∈ v → x_1 = x → y ∈ s
⊢ s ∈ 𝓝 (x, y).snd
[PROOFSTEP]
exact mem_of_superset hv fun z hz => H _ (mem_of_mem_nhds hu) _ hz rfl
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
⊢ IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
[PROOFSTEP]
cases' (s ×ˢ t).eq_empty_or_nonempty with h h
[GOAL]
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
[PROOFSTEP]
simp [h, prod_eq_empty_iff.1 h]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
⊢ IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
[PROOFSTEP]
have st : s.Nonempty ∧ t.Nonempty := prod_nonempty_iff.1 h
[GOAL]
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
[PROOFSTEP]
constructor
[GOAL]
case inr.mp
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ IsOpen (s ×ˢ t) → IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
[PROOFSTEP]
intro (H : IsOpen (s ×ˢ t))
[GOAL]
case inr.mp
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
[PROOFSTEP]
refine' Or.inl ⟨_, _⟩
[GOAL]
case inr.mp.refine'_1
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen s
case inr.mp.refine'_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen t
[PROOFSTEP]
show IsOpen s
[GOAL]
case inr.mp.refine'_1
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen s
[PROOFSTEP]
rw [← fst_image_prod s st.2]
[GOAL]
case inr.mp.refine'_1
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen (Prod.fst '' s ×ˢ t)
[PROOFSTEP]
exact isOpenMap_fst _ H
[GOAL]
case inr.mp.refine'_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen t
[PROOFSTEP]
show IsOpen t
[GOAL]
case inr.mp.refine'_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen t
[PROOFSTEP]
rw [← snd_image_prod st.1 t]
[GOAL]
case inr.mp.refine'_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen (Prod.snd '' s ×ˢ t)
[PROOFSTEP]
exact isOpenMap_snd _ H
[GOAL]
case inr.mpr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅ → IsOpen (s ×ˢ t)
[PROOFSTEP]
intro H
[GOAL]
case inr.mpr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
⊢ IsOpen (s ×ˢ t)
[PROOFSTEP]
simp only [st.1.ne_empty, st.2.ne_empty, not_false_iff, or_false_iff] at H 
[GOAL]
case inr.mpr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen s ∧ IsOpen t
⊢ IsOpen (s ×ˢ t)
[PROOFSTEP]
exact H.1.prod H.2
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
x✝ : α × β
a : α
b : β
⊢ (a, b) ∈ closure (s ×ˢ t) ↔ (a, b) ∈ closure s ×ˢ closure t
[PROOFSTEP]
simp_rw [mem_prod, mem_closure_iff_nhdsWithin_neBot, nhdsWithin_prod_eq, prod_neBot]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
x✝ : α × β
a : α
b : β
⊢ (a, b) ∈ interior (s ×ˢ t) ↔ (a, b) ∈ interior s ×ˢ interior t
[PROOFSTEP]
simp only [mem_interior_iff_mem_nhds, mem_prod, prod_mem_nhds_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
⊢ frontier (s ×ˢ t) = closure s ×ˢ frontier t ∪ frontier s ×ˢ closure t
[PROOFSTEP]
simp only [frontier, closure_prod_eq, interior_prod_eq, prod_diff_prod]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
⊢ frontier (s ×ˢ univ) = frontier s ×ˢ univ
[PROOFSTEP]
simp [frontier_prod_eq]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set β
⊢ frontier (univ ×ˢ s) = univ ×ˢ frontier s
[PROOFSTEP]
simp [frontier_prod_eq]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β → γ
a : α
b : β
s : Set α
t : Set β
u : Set γ
hf : Continuous (uncurry f)
ha : a ∈ closure s
hb : b ∈ closure t
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a b ∈ u
⊢ (a, b) ∈ closure (s ×ˢ t)
[PROOFSTEP]
simpa only [closure_prod_eq] using mk_mem_prod ha hb
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s₁ : Set α
s₂ : Set β
h₁ : IsClosed s₁
h₂ : IsClosed s₂
⊢ closure (s₁ ×ˢ s₂) = s₁ ×ˢ s₂
[PROOFSTEP]
simp only [h₁.closure_eq, h₂.closure_eq, closure_prod_eq]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
hs : Dense s
ht : Dense t
x : α × β
⊢ x ∈ closure (s ×ˢ t)
[PROOFSTEP]
rw [closure_prod_eq]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
hs : Dense s
ht : Dense t
x : α × β
⊢ x ∈ closure s ×ˢ closure t
[PROOFSTEP]
exact ⟨hs x.1, ht x.2⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
ι : Type u_5
κ : Type u_6
f : ι → β
g : κ → γ
hf : DenseRange f
hg : DenseRange g
⊢ DenseRange (Prod.map f g)
[PROOFSTEP]
simpa only [DenseRange, prod_range_range_eq] using hf.prod hg
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : Inducing f
hg : Inducing g
x✝ : α × γ
a : α
b : γ
⊢ 𝓝 (a, b) = comap (Prod.map f g) (𝓝 (Prod.map f g (a, b)))
[PROOFSTEP]
simp_rw [Prod.map, nhds_prod_eq, hf.nhds_eq_comap, hg.nhds_eq_comap, prod_comap_comap_eq]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
f : β → γ
⊢ (Inducing fun x => (a, f x)) ↔ Inducing f
[PROOFSTEP]
simp_rw [inducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose, Function.comp, induced_const, top_inf_eq]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
b : β
f : α → γ
⊢ (Inducing fun x => (f x, b)) ↔ Inducing f
[PROOFSTEP]
simp_rw [inducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose, Function.comp, induced_const, inf_top_eq]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : _root_.Embedding f
hg : _root_.Embedding g
src✝ : Inducing (Prod.map f g) := Inducing.prod_map hf.toInducing hg.toInducing
x✝¹ x✝ : α × γ
x₁ : α
x₂ : γ
y₁ : α
y₂ : γ
⊢ Prod.map f g (x₁, x₂) = Prod.map f g (y₁, y₂) → (x₁, x₂) = (y₁, y₂)
[PROOFSTEP]
simp [hf.inj.eq_iff, hg.inj.eq_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : IsOpenMap f
hg : IsOpenMap g
⊢ IsOpenMap fun p => (f p.fst, g p.snd)
[PROOFSTEP]
rw [isOpenMap_iff_nhds_le]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : IsOpenMap f
hg : IsOpenMap g
⊢ ∀ (a : α × γ), 𝓝 (f a.fst, g a.snd) ≤ map (fun p => (f p.fst, g p.snd)) (𝓝 a)
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : IsOpenMap f
hg : IsOpenMap g
a : α
b : γ
⊢ 𝓝 (f (a, b).fst, g (a, b).snd) ≤ map (fun p => (f p.fst, g p.snd)) (𝓝 (a, b))
[PROOFSTEP]
rw [nhds_prod_eq, nhds_prod_eq, ← Filter.prod_map_map_eq]
[GOAL]
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : IsOpenMap f
hg : IsOpenMap g
a : α
b : γ
⊢ 𝓝 (f (a, b).fst) ×ˢ 𝓝 (g (a, b).snd) ≤ map f (𝓝 a) ×ˢ map g (𝓝 b)
[PROOFSTEP]
exact Filter.prod_mono (hf.nhds_le a) (hg.nhds_le b)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set (α ⊕ β)
⊢ IsClosed s ↔ IsClosed (inl ⁻¹' s) ∧ IsClosed (inr ⁻¹' s)
[PROOFSTEP]
simp only [← isOpen_compl_iff, isOpen_sum_iff, preimage_compl]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
u : Set α
hu : IsOpen u
⊢ IsOpen (inl '' u)
[PROOFSTEP]
simpa [isOpen_sum_iff, preimage_image_eq u Sum.inl_injective]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
u : Set β
hu : IsOpen u
⊢ IsOpen (inr '' u)
[PROOFSTEP]
simpa [isOpen_sum_iff, preimage_image_eq u Sum.inr_injective]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
⊢ IsClosed (range inl)
[PROOFSTEP]
rw [← isOpen_compl_iff, compl_range_inl]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
⊢ IsOpen (range inr)
[PROOFSTEP]
exact isOpen_range_inr
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
⊢ IsClosed (range inr)
[PROOFSTEP]
rw [← isOpen_compl_iff, compl_range_inr]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
⊢ IsOpen (range inl)
[PROOFSTEP]
exact isOpen_range_inl
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α ⊕ β → γ
⊢ IsOpenMap f ↔ (IsOpenMap fun a => f (inl a)) ∧ IsOpenMap fun b => f (inr b)
[PROOFSTEP]
simp only [isOpenMap_iff_nhds_le, Sum.forall, nhds_inl, nhds_inr, Filter.map_map, comp]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → γ
g : β → γ
⊢ IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g
[PROOFSTEP]
simp only [isOpenMap_sum, elim_inl, elim_inr]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
h : IsClosed {a | p a}
⊢ IsClosed (range Subtype.val)
[PROOFSTEP]
rwa [Subtype.range_coe_subtype]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
f : α → β
hcl : IsClosedMap f
T : Set β
⊢ IsClosedMap (Set.restrictPreimage T f)
[PROOFSTEP]
rw [isClosedMap_iff_clusterPt] at hcl ⊢
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
f : α → β
hcl : ∀ (s : Set α) (y : β), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
T : Set β
⊢ ∀ (s : Set ↑(f ⁻¹' T)) (y : ↑T),
    MapClusterPt y (𝓟 s) (Set.restrictPreimage T f) → ∃ x, Set.restrictPreimage T f x = y ∧ ClusterPt x (𝓟 s)
[PROOFSTEP]
intro A ⟨y, hyT⟩ hy
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
f : α → β
hcl : ∀ (s : Set α) (y : β), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
T : Set β
A : Set ↑(f ⁻¹' T)
y : β
hyT : y ∈ T
hy : MapClusterPt { val := y, property := hyT } (𝓟 A) (Set.restrictPreimage T f)
⊢ ∃ x, Set.restrictPreimage T f x = { val := y, property := hyT } ∧ ClusterPt x (𝓟 A)
[PROOFSTEP]
rw [restrictPreimage, MapClusterPt, ← inducing_subtype_val.mapClusterPt_iff, MapClusterPt, map_map,
  MapsTo.restrict_commutes, ← map_map, ← MapClusterPt, map_principal] at hy 
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
f : α → β
hcl : ∀ (s : Set α) (y : β), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
T : Set β
A : Set ↑(f ⁻¹' T)
y : β
hyT : y ∈ T
hy : MapClusterPt (↑{ val := y, property := hyT }) (𝓟 (Subtype.val '' A)) f
⊢ ∃ x, Set.restrictPreimage T f x = { val := y, property := hyT } ∧ ClusterPt x (𝓟 A)
[PROOFSTEP]
rcases hcl _ y hy with ⟨x, hxy, hx⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
f : α → β
hcl : ∀ (s : Set α) (y : β), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
T : Set β
A : Set ↑(f ⁻¹' T)
y : β
hyT : y ∈ T
hy : MapClusterPt (↑{ val := y, property := hyT }) (𝓟 (Subtype.val '' A)) f
x : α
hxy : f x = y
hx : ClusterPt x (𝓟 (Subtype.val '' A))
⊢ ∃ x, Set.restrictPreimage T f x = { val := y, property := hyT } ∧ ClusterPt x (𝓟 A)
[PROOFSTEP]
have hxT : f x ∈ T := hxy ▸ hyT
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
f : α → β
hcl : ∀ (s : Set α) (y : β), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
T : Set β
A : Set ↑(f ⁻¹' T)
y : β
hyT : y ∈ T
hy : MapClusterPt (↑{ val := y, property := hyT }) (𝓟 (Subtype.val '' A)) f
x : α
hxy : f x = y
hx : ClusterPt x (𝓟 (Subtype.val '' A))
hxT : f x ∈ T
⊢ ∃ x, Set.restrictPreimage T f x = { val := y, property := hyT } ∧ ClusterPt x (𝓟 A)
[PROOFSTEP]
refine ⟨⟨x, hxT⟩, Subtype.ext hxy, ?_⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
f : α → β
hcl : ∀ (s : Set α) (y : β), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
T : Set β
A : Set ↑(f ⁻¹' T)
y : β
hyT : y ∈ T
hy : MapClusterPt (↑{ val := y, property := hyT }) (𝓟 (Subtype.val '' A)) f
x : α
hxy : f x = y
hx : ClusterPt x (𝓟 (Subtype.val '' A))
hxT : f x ∈ T
⊢ ClusterPt { val := x, property := hxT } (𝓟 A)
[PROOFSTEP]
rwa [← inducing_subtype_val.mapClusterPt_iff, MapClusterPt, map_principal]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
s : Set α
t : Set ↑s
⊢ Dense t ↔ s ⊆ closure (val '' t)
[PROOFSTEP]
rw [inducing_subtype_val.dense_iff, SetCoe.forall]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
s : Set α
t : Set ↑s
⊢ (∀ (x : α) (h : x ∈ s), ↑{ val := x, property := h } ∈ closure (val '' t)) ↔ s ⊆ closure (val '' t)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
s : Set α
a : ↑s
⊢ map Subtype.val (𝓝 a) = 𝓝[s] ↑a
[PROOFSTEP]
rw [inducing_subtype_val.map_nhds_eq, Subtype.range_val]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
a : α
ha : p a
h : ∀ᶠ (x : α) in 𝓝 a, p x
⊢ range Subtype.val ∈ 𝓝 ↑{ val := a, property := ha }
[PROOFSTEP]
rw [Subtype.range_val]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
a : α
ha : p a
h : ∀ᶠ (x : α) in 𝓝 a, p x
⊢ (fun x => p x) ∈ 𝓝 ↑{ val := a, property := ha }
[PROOFSTEP]
exact h
[GOAL]
α : Type u
β✝ : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β✝
inst✝ : TopologicalSpace γ
p✝ : α → Prop
β : Type u_5
p : α → Prop
b : Filter β
f : β → Subtype p
a : α
ha : p a
⊢ Tendsto f b (𝓝 { val := a, property := ha }) ↔ Tendsto (fun x => ↑(f x)) b (𝓝 ↑{ val := a, property := ha })
[PROOFSTEP]
rw [nhds_subtype_eq_comap, tendsto_comap_iff]
[GOAL]
α : Type u
β✝ : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β✝
inst✝ : TopologicalSpace γ
p✝ : α → Prop
β : Type u_5
p : α → Prop
b : Filter β
f : β → Subtype p
a : α
ha : p a
⊢ Tendsto (Subtype.val ∘ f) b (𝓝 a) ↔ Tendsto (fun x => ↑(f x)) b (𝓝 ↑{ val := a, property := ha })
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
⊢ Continuous f ↔ ∀ (i : ι), Continuous fun a => f a i
[PROOFSTEP]
simp only [continuous_iInf_rng, continuous_induced_rng, comp]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
a : (i : ι) → π i
⊢ 𝓝 a = Filter.pi fun i => 𝓝 (a i)
[PROOFSTEP]
simp only [nhds_iInf, nhds_induced, Filter.pi]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
f : β → (i : ι) → π i
g : (i : ι) → π i
u : Filter β
⊢ Tendsto f u (𝓝 g) ↔ ∀ (x : ι), Tendsto (fun i => f i x) u (𝓝 (g x))
[PROOFSTEP]
rw [nhds_pi, Filter.tendsto_pi]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
inst✝ : DecidableEq ι
l : Filter β
f : β → (i : ι) → π i
x : (i : ι) → π i
hf : Tendsto f l (𝓝 x)
i : ι
g : β → π i
xi : π i
hg : Tendsto g l (𝓝 xi)
j : ι
⊢ Tendsto (fun i_1 => Function.update (f i_1) i (g i_1) j) l (𝓝 (Function.update x i xi j))
[PROOFSTEP]
rcases eq_or_ne j i with (rfl | hj)
[GOAL]
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
inst✝ : DecidableEq ι
l : Filter β
f : β → (i : ι) → π i
x : (i : ι) → π i
hf : Tendsto f l (𝓝 x)
j : ι
g : β → π j
xi : π j
hg : Tendsto g l (𝓝 xi)
⊢ Tendsto (fun i => Function.update (f i) j (g i) j) l (𝓝 (Function.update x j xi j))
[PROOFSTEP]
simp [*, hf.apply]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
inst✝ : DecidableEq ι
l : Filter β
f : β → (i : ι) → π i
x : (i : ι) → π i
hf : Tendsto f l (𝓝 x)
i : ι
g : β → π i
xi : π i
hg : Tendsto g l (𝓝 xi)
j : ι
hj : j ≠ i
⊢ Tendsto (fun i_1 => Function.update (f i_1) i (g i_1) j) l (𝓝 (Function.update x i xi j))
[PROOFSTEP]
simp [*, hf.apply]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f✝ : α → (i : ι) → π✝ i
n : ℕ
π : Fin (n + 1) → Type u_8
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (π i)
i : Fin (n + 1)
f : β → π i
l : Filter β
x : π i
hf : Tendsto f l (𝓝 x)
g : β → (j : Fin n) → π (Fin.succAbove i j)
y : (j : Fin n) → π (Fin.succAbove i j)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ Tendsto (fun i_1 => Fin.insertNth i (f i_1) (g i_1) i) l (𝓝 (Fin.insertNth i x y i))
[PROOFSTEP]
simpa
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f✝ : α → (i : ι) → π✝ i
n : ℕ
π : Fin (n + 1) → Type u_8
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (π i)
i : Fin (n + 1)
f : β → π i
l : Filter β
x : π i
hf : Tendsto f l (𝓝 x)
g : β → (j : Fin n) → π (Fin.succAbove i j)
y : (j : Fin n) → π (Fin.succAbove i j)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (j : Fin n),
    Tendsto (fun i_1 => Fin.insertNth i (f i_1) (g i_1) (Fin.succAbove i j)) l
      (𝓝 (Fin.insertNth i x y (Fin.succAbove i j)))
[PROOFSTEP]
simpa using tendsto_pi_nhds.1 hg
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
hi : Set.Finite i
hs : ∀ (a : ι), a ∈ i → IsOpen (s a)
⊢ IsOpen (Set.pi i s)
[PROOFSTEP]
rw [pi_def]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
hi : Set.Finite i
hs : ∀ (a : ι), a ∈ i → IsOpen (s a)
⊢ IsOpen (⋂ (a : ι) (_ : a ∈ i), eval a ⁻¹' s a)
[PROOFSTEP]
exact isOpen_biInter hi fun a ha => (hs _ ha).preimage (continuous_apply _)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
⊢ IsOpen s ↔ ∀ (f : (a : ι) → π a), f ∈ s → ∃ I u, (∀ (a : ι), a ∈ I → IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi (↑I) u ⊆ s
[PROOFSTEP]
rw [isOpen_iff_nhds]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
⊢ (∀ (a : (a : ι) → π a), a ∈ s → 𝓝 a ≤ 𝓟 s) ↔
    ∀ (f : (a : ι) → π a), f ∈ s → ∃ I u, (∀ (a : ι), a ∈ I → IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi (↑I) u ⊆ s
[PROOFSTEP]
simp_rw [le_principal_iff, nhds_pi, Filter.mem_pi', mem_nhds_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
⊢ (∀ (a : (a : ι) → π a), a ∈ s → ∃ I t, (∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1) ∧ Set.pi (↑I) t ⊆ s) ↔
    ∀ (f : (a : ι) → π a), f ∈ s → ∃ I u, (∀ (a : ι), a ∈ I → IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi (↑I) u ⊆ s
[PROOFSTEP]
refine ball_congr fun a _ => ⟨?_, ?_⟩
[GOAL]
case refine_1
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
⊢ (∃ I t, (∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1) ∧ Set.pi (↑I) t ⊆ s) →
    ∃ I u, (∀ (a_2 : ι), a_2 ∈ I → IsOpen (u a_2) ∧ a a_2 ∈ u a_2) ∧ Set.pi (↑I) u ⊆ s
[PROOFSTEP]
rintro ⟨I, t, ⟨h1, h2⟩⟩
[GOAL]
case refine_1.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1
h2 : Set.pi (↑I) t ⊆ s
⊢ ∃ I u, (∀ (a_1 : ι), a_1 ∈ I → IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi (↑I) u ⊆ s
[PROOFSTEP]
refine ⟨I, fun a => eval a '' (I : Set ι).pi fun a => (h1 a).choose, fun i hi => ?_, ?_⟩
[GOAL]
case refine_1.intro.intro.intro.refine_1
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1
h2 : Set.pi (↑I) t ⊆ s
i : ι
hi : i ∈ I
⊢ IsOpen
      ((fun a_1 => eval a_1 '' Set.pi ↑I fun a_2 => Exists.choose (_ : ∃ t_1, t_1 ⊆ t a_2 ∧ IsOpen t_1 ∧ a a_2 ∈ t_1))
        i) ∧
    a i ∈
      (fun a_1 => eval a_1 '' Set.pi ↑I fun a_2 => Exists.choose (_ : ∃ t_1, t_1 ⊆ t a_2 ∧ IsOpen t_1 ∧ a a_2 ∈ t_1)) i
[PROOFSTEP]
simp_rw [Set.eval_image_pi (Finset.mem_coe.mpr hi) (pi_nonempty_iff.mpr fun i => ⟨_, fun _ => (h1 i).choose_spec.2.2⟩)]
[GOAL]
case refine_1.intro.intro.intro.refine_1
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1
h2 : Set.pi (↑I) t ⊆ s
i : ι
hi : i ∈ I
⊢ IsOpen (Exists.choose (_ : ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1)) ∧
    a i ∈ Exists.choose (_ : ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1)
[PROOFSTEP]
exact (h1 i).choose_spec.2
[GOAL]
case refine_1.intro.intro.intro.refine_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1
h2 : Set.pi (↑I) t ⊆ s
⊢ (Set.pi ↑I fun a_1 =>
      eval a_1 '' Set.pi ↑I fun a_2 => Exists.choose (_ : ∃ t_1, t_1 ⊆ t a_2 ∧ IsOpen t_1 ∧ a a_2 ∈ t_1)) ⊆
    s
[PROOFSTEP]
exact Subset.trans (Set.pi_mono fun i hi => (Set.eval_image_pi_subset hi).trans (h1 i).choose_spec.1) h2
[GOAL]
case refine_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
⊢ (∃ I u, (∀ (a_1 : ι), a_1 ∈ I → IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi (↑I) u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1) ∧ Set.pi (↑I) t ⊆ s
[PROOFSTEP]
rintro ⟨I, t, ⟨h1, h2⟩⟩
[GOAL]
case refine_2.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ (a_1 : ι), a_1 ∈ I → IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : Set.pi (↑I) t ⊆ s
⊢ ∃ I t, (∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1) ∧ Set.pi (↑I) t ⊆ s
[PROOFSTEP]
refine ⟨I, fun a => ite (a ∈ I) (t a) Set.univ, fun i => ?_, ?_⟩
[GOAL]
case refine_2.intro.intro.intro.refine_1
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ (a_1 : ι), a_1 ∈ I → IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : Set.pi (↑I) t ⊆ s
i : ι
⊢ ∃ t_1, t_1 ⊆ (fun a => if a ∈ I then t a else univ) i ∧ IsOpen t_1 ∧ a i ∈ t_1
[PROOFSTEP]
by_cases hi : i ∈ I
[GOAL]
case pos
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ (a_1 : ι), a_1 ∈ I → IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : Set.pi (↑I) t ⊆ s
i : ι
hi : i ∈ I
⊢ ∃ t_1, t_1 ⊆ (fun a => if a ∈ I then t a else univ) i ∧ IsOpen t_1 ∧ a i ∈ t_1
[PROOFSTEP]
use t i
[GOAL]
case h
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ (a_1 : ι), a_1 ∈ I → IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : Set.pi (↑I) t ⊆ s
i : ι
hi : i ∈ I
⊢ t i ⊆ (fun a => if a ∈ I then t a else univ) i ∧ IsOpen (t i) ∧ a i ∈ t i
[PROOFSTEP]
simp_rw [if_pos hi]
[GOAL]
case h
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ (a_1 : ι), a_1 ∈ I → IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : Set.pi (↑I) t ⊆ s
i : ι
hi : i ∈ I
⊢ t i ⊆ t i ∧ IsOpen (t i) ∧ a i ∈ t i
[PROOFSTEP]
exact ⟨Subset.rfl, (h1 i) hi⟩
[GOAL]
case neg
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ (a_1 : ι), a_1 ∈ I → IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : Set.pi (↑I) t ⊆ s
i : ι
hi : ¬i ∈ I
⊢ ∃ t_1, t_1 ⊆ (fun a => if a ∈ I then t a else univ) i ∧ IsOpen t_1 ∧ a i ∈ t_1
[PROOFSTEP]
use Set.univ
[GOAL]
case h
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ (a_1 : ι), a_1 ∈ I → IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : Set.pi (↑I) t ⊆ s
i : ι
hi : ¬i ∈ I
⊢ univ ⊆ (fun a => if a ∈ I then t a else univ) i ∧ IsOpen univ ∧ a i ∈ univ
[PROOFSTEP]
simp_rw [if_neg hi]
[GOAL]
case h
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ (a_1 : ι), a_1 ∈ I → IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : Set.pi (↑I) t ⊆ s
i : ι
hi : ¬i ∈ I
⊢ univ ⊆ univ ∧ IsOpen univ ∧ a i ∈ univ
[PROOFSTEP]
exact ⟨Subset.rfl, isOpen_univ, mem_univ _⟩
[GOAL]
case refine_2.intro.intro.intro.refine_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ (a_1 : ι), a_1 ∈ I → IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : Set.pi (↑I) t ⊆ s
⊢ (Set.pi ↑I fun a => if a ∈ I then t a else univ) ⊆ s
[PROOFSTEP]
rw [← Set.univ_pi_ite]
[GOAL]
case refine_2.intro.intro.intro.refine_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ (a_1 : ι), a_1 ∈ I → IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : Set.pi (↑I) t ⊆ s
⊢ (Set.pi univ fun i => if i ∈ ↑I then if i ∈ I then t i else univ else univ) ⊆ s
[PROOFSTEP]
simp only [← ite_and, ← Finset.mem_coe, and_self_iff, Set.univ_pi_ite, h2]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
⊢ IsOpen s ↔ ∀ (f : (a : ι) → π a), f ∈ s → ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi univ u ⊆ s
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ IsOpen s ↔ ∀ (f : (a : ι) → π a), f ∈ s → ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi univ u ⊆ s
[PROOFSTEP]
rw [isOpen_iff_nhds]
[GOAL]
case intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ (∀ (a : (a : ι) → π a), a ∈ s → 𝓝 a ≤ 𝓟 s) ↔
    ∀ (f : (a : ι) → π a), f ∈ s → ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi univ u ⊆ s
[PROOFSTEP]
simp_rw [le_principal_iff, nhds_pi, Filter.mem_pi', mem_nhds_iff]
[GOAL]
case intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ (∀ (a : (a : ι) → π a), a ∈ s → ∃ I t, (∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1) ∧ Set.pi (↑I) t ⊆ s) ↔
    ∀ (f : (a : ι) → π a), f ∈ s → ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ Set.pi univ u ⊆ s
[PROOFSTEP]
refine ball_congr fun a _ => ⟨?_, ?_⟩
[GOAL]
case intro.refine_1
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
⊢ (∃ I t, (∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1) ∧ Set.pi (↑I) t ⊆ s) →
    ∃ u, (∀ (a_2 : ι), IsOpen (u a_2) ∧ a a_2 ∈ u a_2) ∧ Set.pi univ u ⊆ s
[PROOFSTEP]
rintro ⟨I, t, ⟨h1, h2⟩⟩
[GOAL]
case intro.refine_1.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1
h2 : Set.pi (↑I) t ⊆ s
⊢ ∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi univ u ⊆ s
[PROOFSTEP]
refine
  ⟨fun i => (h1 i).choose,
    ⟨fun i => (h1 i).choose_spec.2, (Set.pi_mono fun i _ => (h1 i).choose_spec.1).trans (Subset.trans ?_ h2)⟩⟩
[GOAL]
case intro.refine_1.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1
h2 : Set.pi (↑I) t ⊆ s
⊢ (Set.pi univ fun i => t i) ⊆ Set.pi (↑I) t
[PROOFSTEP]
rw [← Set.pi_inter_compl (I : Set ι)]
[GOAL]
case intro.refine_1.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1
h2 : Set.pi (↑I) t ⊆ s
⊢ ((Set.pi ↑I fun i => t i) ∩ Set.pi (↑I)ᶜ fun i => t i) ⊆ Set.pi (↑I) t
[PROOFSTEP]
exact inter_subset_left _ _
[GOAL]
case intro.refine_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
⊢ (∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi univ u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1, t_1 ⊆ t i ∧ IsOpen t_1 ∧ a i ∈ t_1) ∧ Set.pi (↑I) t ⊆ s
[PROOFSTEP]
exact fun ⟨u, ⟨h1, _⟩⟩ => ⟨Finset.univ, u, ⟨fun i => ⟨u i, ⟨rfl.subset, h1 i⟩⟩, by rwa [Finset.coe_univ]⟩⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝¹ : a ∈ s
x✝ : ∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi univ u ⊆ s
u : (a : ι) → Set (π a)
h1 : ∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1
right✝ : Set.pi univ u ⊆ s
⊢ Set.pi (↑Finset.univ) u ⊆ s
[PROOFSTEP]
rwa [Finset.coe_univ]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
hs : ∀ (a : ι), a ∈ i → IsClosed (s a)
⊢ IsClosed (Set.pi i s)
[PROOFSTEP]
rw [pi_def]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
hs : ∀ (a : ι), a ∈ i → IsClosed (s a)
⊢ IsClosed (⋂ (a : ι) (_ : a ∈ i), eval a ⁻¹' s a)
[PROOFSTEP]
exact isClosed_biInter fun a ha => (hs _ ha).preimage (continuous_apply _)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
I : Set ι
s : (i : ι) → Set (π i)
a : (i : ι) → π i
hs : Set.pi I s ∈ 𝓝 a
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)
[PROOFSTEP]
rw [nhds_pi] at hs 
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
I : Set ι
s : (i : ι) → Set (π i)
a : (i : ι) → π i
hs : Set.pi I s ∈ Filter.pi fun i => 𝓝 (a i)
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)
[PROOFSTEP]
exact mem_of_pi_mem_pi hs hi
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
x : (a : ι) → π a
hi : Set.Finite i
hs : ∀ (a : ι), a ∈ i → s a ∈ 𝓝 (x a)
⊢ Set.pi i s ∈ 𝓝 x
[PROOFSTEP]
rw [pi_def, biInter_mem hi]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
x : (a : ι) → π a
hi : Set.Finite i
hs : ∀ (a : ι), a ∈ i → s a ∈ 𝓝 (x a)
⊢ ∀ (i_1 : ι), i_1 ∈ i → eval i_1 ⁻¹' s i_1 ∈ 𝓝 x
[PROOFSTEP]
exact fun a ha => (continuous_apply a).continuousAt (hs a ha)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
I : Set ι
hI : Set.Finite I
s : (i : ι) → Set (π i)
a : (i : ι) → π i
⊢ Set.pi I s ∈ 𝓝 a ↔ ∀ (i : ι), i ∈ I → s i ∈ 𝓝 (a i)
[PROOFSTEP]
rw [nhds_pi, pi_mem_pi_iff hI]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
I : Set ι
hI : Set.Finite I
s : (i : ι) → Set (π i)
⊢ interior (Set.pi I s) = Set.pi I fun i => interior (s i)
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
I : Set ι
hI : Set.Finite I
s : (i : ι) → Set (π i)
a : (i : ι) → π i
⊢ a ∈ interior (Set.pi I s) ↔ a ∈ Set.pi I fun i => interior (s i)
[PROOFSTEP]
simp only [Set.mem_pi, mem_interior_iff_mem_nhds, set_pi_mem_nhds_iff hI]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x : (a : ι) → π a
hs : s ∈ 𝓝 x
y : (a : ι) → π a
⊢ ∃ I, Finset.piecewise I x y ∈ s
[PROOFSTEP]
simp only [nhds_pi, Filter.mem_pi'] at hs 
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
hs : ∃ I t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ Set.pi (↑I) t ⊆ s
⊢ ∃ I, Finset.piecewise I x y ∈ s
[PROOFSTEP]
rcases hs with ⟨I, t, htx, hts⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
I : Finset ι
t : (i : ι) → Set (π i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : Set.pi (↑I) t ⊆ s
⊢ ∃ I, Finset.piecewise I x y ∈ s
[PROOFSTEP]
refine' ⟨I, hts fun i hi => _⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
I : Finset ι
t : (i : ι) → Set (π i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : Set.pi (↑I) t ⊆ s
i : ι
hi : i ∈ ↑I
⊢ Finset.piecewise I x y i ∈ t i
[PROOFSTEP]
simpa [Finset.mem_coe.1 hi] using mem_of_mem_nhds (htx i)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
⊢ Pi.topologicalSpace = generateFrom {t | ∃ s i, (∀ (a : ι), a ∈ i → s a ∈ g a) ∧ t = Set.pi (↑i) s}
[PROOFSTEP]
refine le_antisymm ?_ ?_
[GOAL]
case refine_1
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
⊢ Pi.topologicalSpace ≤ generateFrom {t | ∃ s i, (∀ (a : ι), a ∈ i → s a ∈ g a) ∧ t = Set.pi (↑i) s}
[PROOFSTEP]
apply le_generateFrom
[GOAL]
case refine_1.h
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
⊢ ∀ (s : Set ((a : ι) → π a)), s ∈ {t | ∃ s i, (∀ (a : ι), a ∈ i → s a ∈ g a) ∧ t = Set.pi (↑i) s} → IsOpen s
[PROOFSTEP]
rintro _ ⟨s, i, hi, rfl⟩
[GOAL]
case refine_1.h.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
s : (a : ι) → Set (π a)
i : Finset ι
hi : ∀ (a : ι), a ∈ i → s a ∈ g a
⊢ IsOpen (Set.pi (↑i) s)
[PROOFSTEP]
letI := fun a => generateFrom (g a)
[GOAL]
case refine_1.h.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
s : (a : ι) → Set (π a)
i : Finset ι
hi : ∀ (a : ι), a ∈ i → s a ∈ g a
this : (a : ι) → TopologicalSpace (π a) := fun a => generateFrom (g a)
⊢ IsOpen (Set.pi (↑i) s)
[PROOFSTEP]
exact isOpen_set_pi i.finite_toSet (fun a ha => GenerateOpen.basic _ (hi a ha))
[GOAL]
case refine_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
⊢ generateFrom {t | ∃ s i, (∀ (a : ι), a ∈ i → s a ∈ g a) ∧ t = Set.pi (↑i) s} ≤ Pi.topologicalSpace
[PROOFSTEP]
refine le_iInf fun a => coinduced_le_iff_le_induced.1 <| le_generateFrom fun s hs => ?_
[GOAL]
case refine_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
a : ι
s : Set (π a)
hs : s ∈ g a
⊢ IsOpen s
[PROOFSTEP]
refine GenerateOpen.basic _ ⟨update (fun a => univ) a s, { a }, ?_⟩
[GOAL]
case refine_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
a : ι
s : Set (π a)
hs : s ∈ g a
⊢ (∀ (a_1 : ι), a_1 ∈ {a} → update (fun a => univ) a s a_1 ∈ g a_1) ∧
    (fun f => f a) ⁻¹' s = Set.pi (↑{a}) (update (fun a => univ) a s)
[PROOFSTEP]
simp [hs]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
⊢ Pi.topologicalSpace = Pi.topologicalSpace
[PROOFSTEP]
simp only [generateFrom_setOf_isOpen]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
⊢ Pi.topologicalSpace = generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s}
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ Pi.topologicalSpace = generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s}
[PROOFSTEP]
rw [pi_generateFrom_eq]
[GOAL]
case intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ generateFrom {t | ∃ s i, (∀ (a : ι), a ∈ i → s a ∈ g a) ∧ t = Set.pi (↑i) s} =
    generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s}
[PROOFSTEP]
refine' le_antisymm (generateFrom_anti _) (le_generateFrom _)
[GOAL]
case intro.refine'_1
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s} ⊆
    {t | ∃ s i, (∀ (a : ι), a ∈ i → s a ∈ g a) ∧ t = Set.pi (↑i) s}
[PROOFSTEP]
exact fun s ⟨t, ht, Eq⟩ => ⟨t, Finset.univ, by simp [ht, Eq]⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
s : Set ((i : ι) → π i)
x✝ : s ∈ {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s}
t : (a : ι) → Set (π a)
ht : ∀ (a : ι), t a ∈ g a
Eq : s = Set.pi univ t
⊢ (∀ (a : ι), a ∈ Finset.univ → t a ∈ g a) ∧ s = Set.pi (↑Finset.univ) t
[PROOFSTEP]
simp [ht, Eq]
[GOAL]
case intro.refine'_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ ∀ (s : Set ((i : ι) → π i)), s ∈ {t | ∃ s i, (∀ (a : ι), a ∈ i → s a ∈ g a) ∧ t = Set.pi (↑i) s} → IsOpen s
[PROOFSTEP]
rintro s ⟨t, i, ht, rfl⟩
[GOAL]
case intro.refine'_2.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ (a : ι), a ∈ i → t a ∈ g a
⊢ IsOpen (Set.pi (↑i) t)
[PROOFSTEP]
letI := generateFrom {t | ∃ s : ∀ a, Set (π a), (∀ a, s a ∈ g a) ∧ t = pi univ s}
[GOAL]
case intro.refine'_2.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ (a : ι), a ∈ i → t a ∈ g a
this : TopologicalSpace ((i : ι) → π i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s}
⊢ IsOpen (Set.pi (↑i) t)
[PROOFSTEP]
refine isOpen_iff_forall_mem_open.2 fun f hf => ?_
[GOAL]
case intro.refine'_2.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f✝ : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ (a : ι), a ∈ i → t a ∈ g a
this : TopologicalSpace ((i : ι) → π i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s}
f : (i : ι) → π i
hf : f ∈ Set.pi (↑i) t
⊢ ∃ t_1, t_1 ⊆ Set.pi (↑i) t ∧ IsOpen t_1 ∧ f ∈ t_1
[PROOFSTEP]
choose c hcg hfc using fun a => sUnion_eq_univ_iff.1 (hg a) (f a)
[GOAL]
case intro.refine'_2.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f✝ : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ (a : ι), a ∈ i → t a ∈ g a
this : TopologicalSpace ((i : ι) → π i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s}
f : (i : ι) → π i
hf : f ∈ Set.pi (↑i) t
c : (a : ι) → Set (π a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
⊢ ∃ t_1, t_1 ⊆ Set.pi (↑i) t ∧ IsOpen t_1 ∧ f ∈ t_1
[PROOFSTEP]
refine ⟨pi i t ∩ pi ((↑i)ᶜ : Set ι) c, inter_subset_left _ _, ?_, ⟨hf, fun a _ => hfc a⟩⟩
[GOAL]
case intro.refine'_2.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f✝ : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ (a : ι), a ∈ i → t a ∈ g a
this : TopologicalSpace ((i : ι) → π i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s}
f : (i : ι) → π i
hf : f ∈ Set.pi (↑i) t
c : (a : ι) → Set (π a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
⊢ IsOpen (Set.pi (↑i) t ∩ Set.pi (↑i)ᶜ c)
[PROOFSTEP]
rw [← univ_pi_piecewise]
[GOAL]
case intro.refine'_2.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f✝ : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ (a : ι), a ∈ i → t a ∈ g a
this : TopologicalSpace ((i : ι) → π i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s}
f : (i : ι) → π i
hf : f ∈ Set.pi (↑i) t
c : (a : ι) → Set (π a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
⊢ IsOpen (Set.pi univ (piecewise (↑i) t c))
[PROOFSTEP]
refine GenerateOpen.basic _ ⟨_, fun a => ?_, rfl⟩
[GOAL]
case intro.refine'_2.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f✝ : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ (a : ι), a ∈ i → t a ∈ g a
this : TopologicalSpace ((i : ι) → π i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s}
f : (i : ι) → π i
hf : f ∈ Set.pi (↑i) t
c : (a : ι) → Set (π a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
⊢ piecewise (↑i) t c a ∈ g a
[PROOFSTEP]
by_cases a ∈ i
[GOAL]
case intro.refine'_2.intro.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f✝ : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ (a : ι), a ∈ i → t a ∈ g a
this : TopologicalSpace ((i : ι) → π i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s}
f : (i : ι) → π i
hf : f ∈ Set.pi (↑i) t
c : (a : ι) → Set (π a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
⊢ piecewise (↑i) t c a ∈ g a
[PROOFSTEP]
by_cases a ∈ i
[GOAL]
case pos
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f✝ : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ (a : ι), a ∈ i → t a ∈ g a
this : TopologicalSpace ((i : ι) → π i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s}
f : (i : ι) → π i
hf : f ∈ Set.pi (↑i) t
c : (a : ι) → Set (π a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
h : a ∈ i
⊢ piecewise (↑i) t c a ∈ g a
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π✝ : ι → Type u_6
κ : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f✝ : α → (i : ι) → π✝ i
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ (a : ι), a ∈ i → t a ∈ g a
this : TopologicalSpace ((i : ι) → π i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.pi univ s}
f : (i : ι) → π i
hf : f ∈ Set.pi (↑i) t
c : (a : ι) → Set (π a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
h : ¬a ∈ i
⊢ piecewise (↑i) t c a ∈ g a
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
X : Type u_8
f : X → (i : ι) → π i
⊢ induced f Pi.topologicalSpace = ⨅ (i : ι), induced (fun x => f x i) inferInstance
[PROOFSTEP]
erw [induced_iInf]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
X : Type u_8
f : X → (i : ι) → π i
⊢ ⨅ (i : ι), induced f (induced (fun f => f i) ((fun a => inst✝ a) i)) =
    ⨅ (i : ι), induced (fun x => f x i) inferInstance
[PROOFSTEP]
simp only [induced_compose]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
X : Type u_8
f : X → (i : ι) → π i
⊢ ⨅ (i : ι), induced ((fun f => f i) ∘ f) (inst✝ i) = ⨅ (i : ι), induced (fun x => f x i) inferInstance
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝³ : TopologicalSpace α
inst✝² : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), DiscreteTopology (π i)
x : (i : ι) → π i
⊢ IsOpen {x}
[PROOFSTEP]
rw [← univ_pi_singleton]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
π : ι → Type u_6
κ : Type u_7
inst✝³ : TopologicalSpace α
inst✝² : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), DiscreteTopology (π i)
x : (i : ι) → π i
⊢ IsOpen (Set.pi univ fun i => {x i})
[PROOFSTEP]
exact isOpen_set_pi finite_univ fun i _ => (isOpen_discrete {x i})
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set (Sigma σ)
⊢ IsOpen s ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
[PROOFSTEP]
delta instTopologicalSpaceSigma
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set (Sigma σ)
⊢ IsOpen s ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
[PROOFSTEP]
rw [isOpen_iSup_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set (Sigma σ)
⊢ (∀ (i : ι), IsOpen s) ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set (Sigma σ)
⊢ IsClosed s ↔ ∀ (i : ι), IsClosed (Sigma.mk i ⁻¹' s)
[PROOFSTEP]
simp only [← isOpen_compl_iff, isOpen_sigma_iff, preimage_compl]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
⊢ IsOpenMap (Sigma.mk i)
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
⊢ IsOpen (Sigma.mk i '' s)
[PROOFSTEP]
rw [isOpen_sigma_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
⊢ ∀ (i_1 : ι), IsOpen (Sigma.mk i_1 ⁻¹' (Sigma.mk i '' s))
[PROOFSTEP]
intro j
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
[PROOFSTEP]
rcases eq_or_ne j i with (rfl | hne)
[GOAL]
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
j : ι
s : Set (σ j)
hs : IsOpen s
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk j '' s))
[PROOFSTEP]
rwa [Set.preimage_image_eq _ sigma_mk_injective]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
hne : j ≠ i
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
[PROOFSTEP]
rw [preimage_image_sigmaMk_of_ne hne]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
hne : j ≠ i
⊢ IsOpen ∅
[PROOFSTEP]
exact isOpen_empty
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
⊢ IsClosedMap (Sigma.mk i)
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
⊢ IsClosed (Sigma.mk i '' s)
[PROOFSTEP]
rw [isClosed_sigma_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
⊢ ∀ (i_1 : ι), IsClosed (Sigma.mk i_1 ⁻¹' (Sigma.mk i '' s))
[PROOFSTEP]
intro j
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
[PROOFSTEP]
rcases eq_or_ne j i with (rfl | hne)
[GOAL]
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
j : ι
s : Set (σ j)
hs : IsClosed s
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk j '' s))
[PROOFSTEP]
rwa [Set.preimage_image_eq _ sigma_mk_injective]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
hne : j ≠ i
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
[PROOFSTEP]
rw [preimage_image_sigmaMk_of_ne hne]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
hne : j ≠ i
⊢ IsClosed ∅
[PROOFSTEP]
exact isClosed_empty
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
x : Sigma σ
⊢ 𝓝 x = Filter.map (mk x.fst) (𝓝 x.snd)
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
fst✝ : ι
snd✝ : σ fst✝
⊢ 𝓝 { fst := fst✝, snd := snd✝ } = Filter.map (mk { fst := fst✝, snd := snd✝ }.fst) (𝓝 { fst := fst✝, snd := snd✝ }.snd)
[PROOFSTEP]
apply Sigma.nhds_mk
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set ι
⊢ IsOpen (Sigma.fst ⁻¹' s)
[PROOFSTEP]
rw [← biUnion_of_singleton s, preimage_iUnion₂]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set ι
⊢ IsOpen (⋃ (i : ι) (_ : i ∈ s), Sigma.fst ⁻¹' {i})
[PROOFSTEP]
simp only [← range_sigmaMk]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set ι
⊢ IsOpen (⋃ (i : ι) (_ : i ∈ s), range (Sigma.mk i))
[PROOFSTEP]
exact isOpen_biUnion fun _ _ => isOpen_range_sigmaMk
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
⊢ Continuous f ↔ ∀ (i : ι), Continuous fun a => f { fst := i, snd := a }
[PROOFSTEP]
delta instTopologicalSpaceSigma
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
⊢ Continuous f ↔ ∀ (i : ι), Continuous fun a => f { fst := i, snd := a }
[PROOFSTEP]
rw [continuous_iSup_dom]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
⊢ (∀ (i : ι), Continuous f) ↔ ∀ (i : ι), Continuous fun a => f { fst := i, snd := a }
[PROOFSTEP]
exact forall_congr' fun _ => continuous_coinduced_dom
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
⊢ Inducing f ↔ (∀ (i : ι), Inducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
[PROOFSTEP]
refine ⟨fun h ↦ ⟨fun i ↦ h.comp embedding_sigmaMk.1, fun i ↦ ?_⟩, ?_⟩
[GOAL]
case refine_1
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
h : Inducing f
i : ι
⊢ ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
[PROOFSTEP]
rcases h.isOpen_iff.1 (isOpen_range_sigmaMk (i := i)) with ⟨U, hUo, hU⟩
[GOAL]
case refine_1.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
h : Inducing f
i : ι
U : Set α
hUo : IsOpen U
hU : f ⁻¹' U = range (Sigma.mk i)
⊢ ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
[PROOFSTEP]
refine ⟨U, hUo, ?_⟩
[GOAL]
case refine_1.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
h : Inducing f
i : ι
U : Set α
hUo : IsOpen U
hU : f ⁻¹' U = range (Sigma.mk i)
⊢ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
[PROOFSTEP]
simpa [Set.ext_iff] using hU
[GOAL]
case refine_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
⊢ ((∀ (i : ι), Inducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i) →
    Inducing f
[PROOFSTEP]
refine fun ⟨h₁, h₂⟩ ↦ inducing_iff_nhds.2 fun ⟨i, x⟩ ↦ ?_
[GOAL]
case refine_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
x✝¹ : (∀ (i : ι), Inducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), Inducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
⊢ 𝓝 { fst := i, snd := x } = comap f (𝓝 (f { fst := i, snd := x }))
[PROOFSTEP]
rw [Sigma.nhds_mk, (h₁ i).nhds_eq_comap, comp_apply, ← comap_comap, map_comap_of_mem]
[GOAL]
case refine_2
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
x✝¹ : (∀ (i : ι), Inducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), Inducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
⊢ range (Sigma.mk i) ∈ comap f (𝓝 (f { fst := i, snd := x }))
[PROOFSTEP]
rcases h₂ i with ⟨U, hUo, hU⟩
[GOAL]
case refine_2.intro.intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
x✝¹ : (∀ (i : ι), Inducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), Inducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
U : Set α
hUo : IsOpen U
hU : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
⊢ range (Sigma.mk i) ∈ comap f (𝓝 (f { fst := i, snd := x }))
[PROOFSTEP]
filter_upwards [preimage_mem_comap <| hUo.mem_nhds <| (hU _).2 rfl] with y hy
[GOAL]
case h
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
x✝¹ : (∀ (i : ι), Inducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), Inducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
U : Set α
hUo : IsOpen U
hU : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
y : Sigma σ
hy : y ∈ f ⁻¹' U
⊢ y ∈ range (Sigma.mk i)
[PROOFSTEP]
simpa [hU] using hy
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
⊢ (∀ (i : ι), Continuous fun a => Sigma.map f₁ f₂ { fst := i, snd := a }) ↔ ∀ (i : ι), Continuous (f₂ i)
[PROOFSTEP]
simp only [Sigma.map, embedding_sigmaMk.continuous_iff, comp]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap fun a => f { fst := i, snd := a }
[PROOFSTEP]
simp only [isOpenMap_iff_nhds_le, Sigma.forall, Sigma.nhds_eq, map_map, comp]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h₁ : Injective f₁
⊢ Inducing (Sigma.map f₁ f₂) ↔ ∀ (i : ι), Inducing (f₂ i)
[PROOFSTEP]
simp only [inducing_iff_nhds, Sigma.forall, Sigma.nhds_mk, Sigma.map_mk, ← map_sigma_mk_comap h₁,
  map_inj sigma_mk_injective]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h : Injective f₁
⊢ _root_.Embedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), _root_.Embedding (f₂ i)
[PROOFSTEP]
simp only [embedding_iff, Injective.sigma_map, inducing_sigma_map h, forall_and, h.sigma_map_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h : Injective f₁
⊢ OpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), OpenEmbedding (f₂ i)
[PROOFSTEP]
simp only [openEmbedding_iff_embedding_open, isOpenMap_sigma_map, embedding_sigma_map h, forall_and]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝ : TopologicalSpace α
⊢ IsClosed (range down)
[PROOFSTEP]
simp only [ULift.down_surjective.range_eq, isClosed_univ]
[GOAL]
α : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝ : TopologicalSpace α
β : Set α
γ : Set ↑β
hγ : IsOpen γ
hβ : IsOpen β
⊢ IsOpen (Lean.Internal.coeM γ)
[PROOFSTEP]
rcases isOpen_induced_iff.mp hγ with ⟨δ, hδ, rfl⟩
[GOAL]
case intro.intro
α : Type u
β✝ : Type v
γ : Type u_1
δ✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝ : TopologicalSpace α
β : Set α
hβ : IsOpen β
δ : Set α
hδ : IsOpen δ
hγ : IsOpen (Subtype.val ⁻¹' δ)
⊢ IsOpen (Lean.Internal.coeM (Subtype.val ⁻¹' δ))
[PROOFSTEP]
convert IsOpen.inter hβ hδ
[GOAL]
case h.e'_3
α : Type u
β✝ : Type v
γ : Type u_1
δ✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝ : TopologicalSpace α
β : Set α
hβ : IsOpen β
δ : Set α
hδ : IsOpen δ
hγ : IsOpen (Subtype.val ⁻¹' δ)
⊢ Lean.Internal.coeM (Subtype.val ⁻¹' δ) = β ∩ δ
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h
α : Type u
β✝ : Type v
γ : Type u_1
δ✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝ : TopologicalSpace α
β : Set α
hβ : IsOpen β
δ : Set α
hδ : IsOpen δ
hγ : IsOpen (Subtype.val ⁻¹' δ)
x✝ : α
⊢ x✝ ∈ Lean.Internal.coeM (Subtype.val ⁻¹' δ) ↔ x✝ ∈ β ∩ δ
[PROOFSTEP]
exact ⟨fun h => ⟨coe_subset h, mem_of_mem_coe h⟩, fun ⟨hβ, hδ⟩ => mem_coe_of_mem hβ hδ⟩
[GOAL]
α : Type u
β✝ : Type v
γ✝ : Type u_1
δ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝ : TopologicalSpace α
β : Set α
γ : Set ↑β
hγ : IsClosed γ
hβ : IsClosed β
⊢ IsClosed (Lean.Internal.coeM γ)
[PROOFSTEP]
rcases isClosed_induced_iff.mp hγ with ⟨δ, hδ, rfl⟩
[GOAL]
case intro.intro
α : Type u
β✝ : Type v
γ : Type u_1
δ✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝ : TopologicalSpace α
β : Set α
hβ : IsClosed β
δ : Set α
hδ : IsClosed δ
hγ : IsClosed (Subtype.val ⁻¹' δ)
⊢ IsClosed (Lean.Internal.coeM (Subtype.val ⁻¹' δ))
[PROOFSTEP]
convert IsClosed.inter hβ hδ
[GOAL]
case h.e'_3
α : Type u
β✝ : Type v
γ : Type u_1
δ✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝ : TopologicalSpace α
β : Set α
hβ : IsClosed β
δ : Set α
hδ : IsClosed δ
hγ : IsClosed (Subtype.val ⁻¹' δ)
⊢ Lean.Internal.coeM (Subtype.val ⁻¹' δ) = β ∩ δ
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h
α : Type u
β✝ : Type v
γ : Type u_1
δ✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝ : TopologicalSpace α
β : Set α
hβ : IsClosed β
δ : Set α
hδ : IsClosed δ
hγ : IsClosed (Subtype.val ⁻¹' δ)
x✝ : α
⊢ x✝ ∈ Lean.Internal.coeM (Subtype.val ⁻¹' δ) ↔ x✝ ∈ β ∩ δ
[PROOFSTEP]
exact ⟨fun h => ⟨coe_subset h, mem_of_mem_coe h⟩, fun ⟨hβ, hδ⟩ => mem_coe_of_mem hβ hδ⟩
