ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : Z → X<VAR>g : Z → Y<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => (f x, g x)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X<GOAL>Continuous fun y => (x, y)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>y : Y<GOAL>Continuous fun x => (x, y)
<VAR>X : Type u<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Z<VAR>α : Type u_5<VAR>f : X → α → Z<VAR>s : Set α<VAR>t : Set Z<VAR>ht : IsClosed t<VAR>hf : ∀ a ∈ s, Continuous fun x => f x a<GOAL>IsClosed {x | Set.MapsTo (f x) s t}
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>g : X × Y → Z<VAR>hg : Continuous g<VAR>e : W → X<VAR>he : Continuous e<VAR>f : W → Y<VAR>hf : Continuous f<GOAL>Continuous fun w => g (e w, f w)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>TopologicalSpace ε<VAR>g : X × Y × Z → ε<VAR>hg : Continuous g<VAR>e : W → X<VAR>he : Continuous e<VAR>f : W → Y<VAR>hf : Continuous f<VAR>k : W → Z<VAR>hk : Continuous k<GOAL>Continuous fun w => g (e w, f w, k w)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>TopologicalSpace ε<VAR>TopologicalSpace ζ<VAR>g : X × Y × Z × ζ → ε<VAR>hg : Continuous g<VAR>e : W → X<VAR>he : Continuous e<VAR>f : W → Y<VAR>hf : Continuous f<VAR>k : W → Z<VAR>hk : Continuous k<VAR>l : W → ζ<VAR>hl : Continuous l<GOAL>Continuous fun w => g (e w, f w, k w, l w)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>f : Z → X<VAR>g : W → Y<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun p => (f p.1, g p.2)
<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>Z : Type u_7<VAR>f : X → Y → Z<VAR>ta1 ta2 : TopologicalSpace X<VAR>tb1 tb2 : TopologicalSpace Y<VAR>tc1 : TopologicalSpace Z<VAR>h : Continuous fun p => f p.1 p.2<GOAL>Continuous fun p => f p.1 p.2
<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>Z : Type u_7<VAR>f : X → Y → Z<VAR>tas : Set (TopologicalSpace X)<VAR>tbs : Set (TopologicalSpace Y)<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tc : TopologicalSpace Z<VAR>hX : tX ∈ tas<VAR>hY : tY ∈ tbs<VAR>hf : Continuous fun p => f p.1 p.2<GOAL>Continuous fun p => f p.1 p.2
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>p : X → Prop<VAR>x : X<VAR>h : ∀ᶠ (x : X) in 𝓝 x, p x<VAR>y : Y<GOAL>∀ᶠ (x : X × Y) in 𝓝 (x, y), p x.1
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>p : Y → Prop<VAR>y : Y<VAR>h : ∀ᶠ (x : Y) in 𝓝 y, p x<VAR>x : X<GOAL>∀ᶠ (x : X × Y) in 𝓝 (x, y), p x.2
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>px : X → Prop<VAR>x : X<VAR>hx : ∀ᶠ (x : X) in 𝓝 x, px x<VAR>py : Y → Prop<VAR>y : Y<VAR>hy : ∀ᶠ (y : Y) in 𝓝 y, py y<GOAL>∀ᶠ (p : X × Y) in 𝓝 (x, y), px p.1 ∧ py p.2
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Continuous Prod.swap
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsClosedMap Prod.swap
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y → Z<VAR>x : X<VAR>h : Continuous (Function.uncurry f)<GOAL>Continuous (f x)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y → Z<VAR>y : Y<VAR>h : Continuous (Function.uncurry f)<GOAL>Continuous fun a => f a y
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>g : X × Y → Z<VAR>x : X<VAR>h : Continuous g<GOAL>Continuous (Function.curry g x)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<VAR>hs : IsOpen s<VAR>ht : IsOpen t<GOAL>IsOpen (s ×ˢ t)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X<VAR>y : Y<GOAL>𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X<VAR>y : Y<VAR>s : Set X<VAR>t : Set Y<GOAL>𝓝[s ×ˢ t] (x, y) = 𝓝[s] x ×ˢ 𝓝[t] y
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X<VAR>y : Y<VAR>s : Set (X × Y)<GOAL>s ∈ 𝓝 (x, y) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X<VAR>y : Y<VAR>s : Set (X × Y)<VAR>tx : Set X<VAR>ty : Set Y<GOAL>s ∈ 𝓝[tx ×ˢ ty] (x, y) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>ιX : Type u_5<VAR>ιY : Type u_6<VAR>px : ιX → Prop<VAR>py : ιY → Prop<VAR>sx : ιX → Set X<VAR>sy : ιY → Set Y<VAR>x : X<VAR>y : Y<VAR>hx : (𝓝 x).HasBasis px sx<VAR>hy : (𝓝 y).HasBasis py sy<GOAL>(𝓝 (x, y)).HasBasis (fun i => px i.1 ∧ py i.2) fun i => sx i.1 ×ˢ sy i.2
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>ιX : Type u_5<VAR>ιY : Type u_6<VAR>pX : ιX → Prop<VAR>pY : ιY → Prop<VAR>sx : ιX → Set X<VAR>sy : ιY → Set Y<VAR>p : X × Y<VAR>hx : (𝓝 p.1).HasBasis pX sx<VAR>hy : (𝓝 p.2).HasBasis pY sy<GOAL>(𝓝 p).HasBasis (fun i => pX i.1 ∧ pY i.2) fun i => sx i.1 ×ˢ sy i.2
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X<VAR>y : Y<VAR>s : Set (X × Y)<GOAL>s ∈ 𝓝 (x, y) ↔ ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧ u ×ˢ v ⊆ s
<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>X : Type u_5<VAR>seq : X → Y × Z<VAR>f : Filter X<VAR>p : Y × Z<GOAL>Filter.Tendsto seq f (𝓝 p) ↔ Filter.Tendsto (fun n => (seq n).1) f (𝓝 p.1) ∧ Filter.Tendsto (fun n => (seq n).2) f (𝓝 p.2)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<VAR>x : X<VAR>y : Y<GOAL>s ×ˢ t ∈ 𝓝 (x, y) ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<VAR>x : X<VAR>y : Y<VAR>hx : s ∈ 𝓝 x<VAR>hy : t ∈ 𝓝 y<GOAL>s ×ˢ t ∈ 𝓝 (x, y)
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsOpen {p | Disjoint (𝓝 p.1) (𝓝 p.2)}
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>p : X → Prop<VAR>q : Y → Prop<VAR>x : X<VAR>y : Y<VAR>hx : ∀ᶠ (x : X) in 𝓝 x, p x<VAR>hy : ∀ᶠ (y : Y) in 𝓝 y, q y<GOAL>∀ᶠ (z : X × Y) in 𝓝 (x, y), p z.1 ∧ q z.2
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X<VAR>y : Y<GOAL>𝓝 (x, y) = Filter.map Prod.swap (𝓝 (y, x))
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>γ : Type u_5<VAR>x : X<VAR>y : Y<VAR>f : Filter γ<VAR>mx : γ → X<VAR>my : γ → Y<VAR>hx : Filter.Tendsto mx f (𝓝 x)<VAR>hy : Filter.Tendsto my f (𝓝 y)<GOAL>Filter.Tendsto (fun c => (mx c, my c)) f (𝓝 (x, y))
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>p : X × Y → Prop<VAR>x : X<VAR>y : Y<VAR>h : ∀ᶠ (x : X × Y) in 𝓝 (x, y), p x<GOAL>∀ᶠ (x' : X) in 𝓝 x, ∀ᶠ (y' : Y) in 𝓝 y, p (x', y')
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y<VAR>g : X → Z<VAR>x : X<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (fun x => (f x, g x)) x
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>f : X → Z<VAR>g : Y → W<VAR>p : X × Y<VAR>hf : ContinuousAt f p.1<VAR>hg : ContinuousAt g p.2<GOAL>ContinuousAt (fun p => (f p.1, g p.2)) p
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>f : X → Z<VAR>g : Y → W<VAR>x : X<VAR>y : Y<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g y<GOAL>ContinuousAt (fun p => (f p.1, g p.2)) (x, y)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>f : Y × Z → W<VAR>g : X → Y<VAR>h : X → Z<VAR>x : X<VAR>hf : ContinuousAt f (g x, h x)<VAR>hg : ContinuousAt g x<VAR>hh : ContinuousAt h x<GOAL>ContinuousAt (fun x => f (g x, h x)) x
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>f : Y × Z → W<VAR>g : X → Y<VAR>h : X → Z<VAR>x : X<VAR>y : Y × Z<VAR>hf : ContinuousAt f y<VAR>hg : ContinuousAt g x<VAR>hh : ContinuousAt h x<VAR>e : (g x, h x) = y<GOAL>ContinuousAt (fun x => f (g x, h x)) x
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X × Y → Z<VAR>hf : Continuous f<VAR>y : Y<GOAL>Continuous fun x => f (x, y)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X × Y → Z<VAR>hf : Continuous f<VAR>x : X<GOAL>Continuous fun y => f (x, y)
<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>s : Set (Set X)<VAR>t : Set (Set Y)<VAR>hs : ⋃₀ s = Set.univ<VAR>ht : ⋃₀ t = Set.univ<GOAL>instTopologicalSpaceProd = TopologicalSpace.generateFrom (Set.image2 (fun x x_1 => x ×ˢ x_1) s t)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>instTopologicalSpaceProd = TopologicalSpace.generateFrom {g | ∃ s t, IsOpen s ∧ IsOpen t ∧ g = s ×ˢ t}
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set (X × Y)<GOAL>IsOpen s ↔ ∀ (a : X) (b : Y), (a, b) ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>TopologicalSpace Y<VAR>TopologicalSpace W<VAR>f : X → Y<VAR>g : Z → W<GOAL>instTopologicalSpaceProd = TopologicalSpace.induced (fun p => (f p.1, g p.2)) instTopologicalSpaceProd
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set (X × X)<VAR>x : X<VAR>hx : s ∈ 𝓝 (x, x)<GOAL>∃ U, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X × Y<GOAL>Filter.map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x) = 𝓝 x.1
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X × Y<GOAL>Filter.map Prod.fst (𝓝 x) = 𝓝 x.1
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsOpenMap Prod.fst
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X × Y<GOAL>Filter.map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x) = 𝓝 x.2
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X × Y<GOAL>Filter.map Prod.snd (𝓝 x) = 𝓝 x.2
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsOpenMap Prod.snd
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<GOAL>IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<GOAL>closure (s ×ˢ t) = closure s ×ˢ closure t
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<GOAL>interior (s ×ˢ t) = interior s ×ˢ interior t
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<GOAL>frontier (s ×ˢ t) = closure s ×ˢ frontier t ∪ frontier s ×ˢ closure t
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<GOAL>frontier (s ×ˢ Set.univ) = frontier s ×ˢ Set.univ
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set Y<GOAL>frontier (Set.univ ×ˢ s) = Set.univ ×ˢ frontier s
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y → Z<VAR>x : X<VAR>y : Y<VAR>s : Set X<VAR>t : Set Y<VAR>u : Set Z<VAR>hf : Continuous (Function.uncurry f)<VAR>hx : x ∈ closure s<VAR>hy : y ∈ closure t<VAR>h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u<GOAL>f x y ∈ closure u
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s₁ : Set X<VAR>s₂ : Set Y<VAR>h₁ : IsClosed s₁<VAR>h₂ : IsClosed s₂<GOAL>IsClosed (s₁ ×ˢ s₂)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<VAR>hs : Dense s<VAR>ht : Dense t<GOAL>Dense (s ×ˢ t)
<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>f : ι → Y<VAR>g : κ → Z<VAR>hf : DenseRange f<VAR>hg : DenseRange g<GOAL>DenseRange (Prod.map f g)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>f : X → Y<VAR>g : Z → W<VAR>hf : Inducing f<VAR>hg : Inducing g<GOAL>Inducing (Prod.map f g)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>x : X<VAR>f : Y → Z<GOAL>(Inducing fun x' => (x, f x')) ↔ Inducing f
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>y : Y<VAR>f : X → Z<GOAL>(Inducing fun x => (f x, y)) ↔ Inducing f
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>f : X → Y<VAR>g : Z → W<VAR>hf : Embedding f<VAR>hg : Embedding g<GOAL>Embedding (Prod.map f g)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>f : X → Y<VAR>g : Z → W<VAR>hf : IsOpenMap f<VAR>hg : IsOpenMap g<GOAL>IsOpenMap fun p => (f p.1, g p.2)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>f : X → Y<VAR>g : Z → W<VAR>hf : OpenEmbedding f<VAR>hg : OpenEmbedding g<GOAL>OpenEmbedding fun x => (f x.1, g x.2)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>Embedding fun x => (x, f x)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X<GOAL>Embedding (Prod.mk x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>f : X → Bool<VAR>b : Bool<GOAL>Continuous f ↔ IsClopen (f ⁻¹' {b})
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X ⊕ Y → Z<GOAL>Continuous f ↔ Continuous (f ∘ Sum.inl) ∧ Continuous (f ∘ Sum.inr)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Z<VAR>g : Y → Z<GOAL>Continuous (Sum.elim f g) ↔ Continuous f ∧ Continuous g
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Z<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous (Sum.elim f g)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Continuous Sum.isLeft
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Continuous Sum.isRight
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Continuous Sum.inl
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Continuous Sum.inr
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set (X ⊕ Y)<GOAL>IsOpen s ↔ IsOpen (Sum.inl ⁻¹' s) ∧ IsOpen (Sum.inr ⁻¹' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set (X ⊕ Y)<GOAL>IsClosed s ↔ IsClosed (Sum.inl ⁻¹' s) ∧ IsClosed (Sum.inr ⁻¹' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsOpenMap Sum.inl
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsOpenMap Sum.inr
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>OpenEmbedding Sum.inl
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>OpenEmbedding Sum.inr
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Embedding Sum.inl
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Embedding Sum.inr
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsOpen (Set.range Sum.inl)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsOpen (Set.range Sum.inr)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsClosed (Set.range Sum.inl)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsClosed (Set.range Sum.inr)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>ClosedEmbedding Sum.inl
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>ClosedEmbedding Sum.inr
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X<GOAL>𝓝 (Sum.inl x) = Filter.map Sum.inl (𝓝 x)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>y : Y<GOAL>𝓝 (Sum.inr y) = Filter.map Sum.inr (𝓝 y)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>f : X → Y<VAR>g : Z → W<GOAL>Continuous (Sum.map f g) ↔ Continuous f ∧ Continuous g
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>f : X → Y<VAR>g : Z → W<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous (Sum.map f g)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X ⊕ Y → Z<GOAL>IsOpenMap f ↔ (IsOpenMap fun a => f (Sum.inl a)) ∧ IsOpenMap fun b => f (Sum.inr b)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Z<VAR>g : Y → Z<GOAL>IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Z<VAR>g : Y → Z<VAR>hf : IsOpenMap f<VAR>hg : IsOpenMap g<GOAL>IsOpenMap (Sum.elim f g)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X ⊕ Y → Z<GOAL>IsClosedMap f ↔ (IsClosedMap fun a => f (Sum.inl a)) ∧ IsClosedMap fun b => f (Sum.inr b)
<VAR>Y : Type v<VAR>TopologicalSpace Y<VAR>t : Set Y<GOAL>Inducing Subtype.val
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>t : Set Y<VAR>ht : ∀ (x : X), f x ∈ t<VAR>h : Inducing (Set.codRestrict f t ht)<GOAL>Inducing f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p : X → Prop<GOAL>Embedding Subtype.val
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p : X → Prop<VAR>h : IsClosed {a | p a}<GOAL>ClosedEmbedding Subtype.val
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p : X → Prop<GOAL>Continuous Subtype.val
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>p : X → Prop<VAR>f : Y → Subtype p<VAR>hf : Continuous f<GOAL>Continuous fun x => ↑(f x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>OpenEmbedding Subtype.val
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>IsOpenMap Subtype.val
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : IsOpenMap f<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>IsOpenMap (s.restrict f)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>ClosedEmbedding Subtype.val
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>IsClosedMap Subtype.val
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>p : X → Prop<VAR>f : Y → X<VAR>h : Continuous f<VAR>hp : ∀ (x : Y), p (f x)<GOAL>Continuous fun x => ⟨f x, ⋯⟩
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>p : X → Prop<VAR>f : X → Y<VAR>h : Continuous f<VAR>q : Y → Prop<VAR>hpq : ∀ (x : X), p x → q (f x)<GOAL>Continuous (Subtype.map f hpq)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>h : s ⊆ t<GOAL>Continuous (Set.inclusion h)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p : X → Prop<VAR>x : Subtype p<GOAL>ContinuousAt Subtype.val x
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>t : Set ↑s<GOAL>Dense t ↔ s ⊆ closure (Subtype.val '' t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>x : ↑s<GOAL>Filter.map Subtype.val (𝓝 x) = 𝓝[s] ↑x
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p : X → Prop<VAR>x : X<VAR>hx : p x<VAR>h : ∀ᶠ (x : X) in 𝓝 x, p x<GOAL>Filter.map Subtype.val (𝓝 ⟨x, hx⟩) = 𝓝 x
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p : X → Prop<VAR>x : X<VAR>h : p x<GOAL>𝓝 ⟨x, h⟩ = Filter.comap Subtype.val (𝓝 x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>Y : Type u_5<VAR>p : X → Prop<VAR>l : Filter Y<VAR>f : Y → Subtype p<VAR>x : Subtype p<GOAL>Filter.Tendsto f l (𝓝 x) ↔ Filter.Tendsto (fun x => ↑(f x)) l (𝓝 ↑x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p : X → Prop<VAR>x : { a // p a }<VAR>s : Set { a // p a }<GOAL>x ∈ closure s ↔ ↑x ∈ closure (Subtype.val '' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>t : Set Y<VAR>h1 : ∀ (x : X), f x ∈ t<VAR>x : X<GOAL>ContinuousAt (Set.codRestrict f t h1) x ↔ ContinuousAt f x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>h1 : Set.MapsTo f s t<VAR>x : ↑s<VAR>h2 : ContinuousAt f ↑x<GOAL>ContinuousAt (Set.MapsTo.restrict f s t h1) x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set Y<VAR>x : ↑(f ⁻¹' s)<VAR>h : ContinuousAt f ↑x<GOAL>ContinuousAt (s.restrictPreimage f) x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set Y<VAR>hf : Continuous f<VAR>hs : ∀ (a : X), f a ∈ s<GOAL>Continuous (Set.codRestrict f s hs)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>h1 : Set.MapsTo f s t<VAR>h2 : Continuous f<GOAL>Continuous (Set.MapsTo.restrict f s t h1)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set Y<VAR>h : Continuous f<GOAL>Continuous (s.restrictPreimage f)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X → Y<VAR>he : Inducing e<VAR>s : Set Y<VAR>hs : ∀ (x : X), e x ∈ s<GOAL>Inducing (Set.codRestrict e s hs)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X → Y<VAR>he : Embedding e<VAR>s : Set Y<VAR>hs : ∀ (x : X), e x ∈ s<GOAL>Embedding (Set.codRestrict e s hs)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>h : s ⊆ t<GOAL>Embedding (Set.inclusion h)
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>DiscreteTopology ↑s → t ⊆ s → DiscreteTopology ↑t
<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set Y<VAR>DiscreteTopology ↑s<VAR>f : X → Y<VAR>hc : Continuous f<VAR>hinj : Function.Injective f<GOAL>DiscreteTopology ↑(f ⁻¹' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : QuotientMap f<VAR>s : Set Y<VAR>hs : IsOpen s<GOAL>QuotientMap (s.restrictPreimage f)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>IsClosed (Subtype.val ⁻¹' t) ↔ s ∩ closure (s ∩ t) ⊆ t
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>r : X → X → Prop<GOAL>QuotientMap (Quot.mk r)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>r : X → X → Prop<GOAL>Continuous (Quot.mk r)