ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>r : X → X → Prop<VAR>f : X → Y<VAR>hr : ∀ (a b : X), r a b → f a = f b<VAR>h : Continuous f<GOAL>Continuous (Quot.lift f hr)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Setoid X<GOAL>QuotientMap Quotient.mk'
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Setoid X<GOAL>Continuous Quotient.mk'
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Setoid X<VAR>f : X → Y<VAR>h : Continuous f<VAR>hs : ∀ (a b : X), a ≈ b → f a = f b<GOAL>Continuous (Quotient.lift f hs)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Setoid X<VAR>f : X → Y<VAR>h : Continuous f<VAR>hs : ∀ (a b : X), Setoid.r a b → f a = f b<GOAL>Continuous fun x => x.liftOn' f hs
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Setoid X<VAR>t : Setoid Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>H : (Setoid.r ⇒ Setoid.r) f f<GOAL>Continuous (Quotient.map' f H)
<VAR>X : Type u<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<GOAL>Continuous f ↔ ∀ (i : ι), Continuous fun a => f a i
<VAR>X : Type u<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>h : ∀ (i : ι), Continuous fun a => f a i<GOAL>Continuous f
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>i : ι<GOAL>Continuous fun p => p i
<VAR>ι : Type u_5<VAR>κ : Type u_7<VAR>ρ : κ → ι → Type u_8<VAR>(j : κ) → (i : ι) → TopologicalSpace (ρ j i)<VAR>j : κ<VAR>i : ι<GOAL>Continuous fun p => p j i
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>i : ι<VAR>x : (i : ι) → π i<GOAL>ContinuousAt (fun p => p i) x
<VAR>Y : Type v<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>l : Filter Y<VAR>f : Y → (i : ι) → π i<VAR>x : (i : ι) → π i<VAR>h : Filter.Tendsto f l (𝓝 x)<VAR>i : ι<GOAL>Filter.Tendsto (fun a => f a i) l (𝓝 (x i))
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>a : (i : ι) → π i<GOAL>𝓝 a = Filter.pi fun i => 𝓝 (a i)
<VAR>Y : Type v<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : Y → (i : ι) → π i<VAR>g : (i : ι) → π i<VAR>u : Filter Y<GOAL>Filter.Tendsto f u (𝓝 g) ↔ ∀ (x : ι), Filter.Tendsto (fun i => f i x) u (𝓝 (g x))
<VAR>X : Type u<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>x : X<GOAL>ContinuousAt f x ↔ ∀ (i : ι), ContinuousAt (fun y => f y i) x
<VAR>X : Type u<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>x : X<VAR>hf : ∀ (i : ι), ContinuousAt (fun y => f y i) x<GOAL>ContinuousAt f x
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>ι' : Type u_8<VAR>φ : ι' → ι<GOAL>Continuous fun f j => f (φ j)
<VAR>X : Type u<VAR>ι : Type u_5<VAR>TopologicalSpace X<VAR>ι' : Type u_8<VAR>φ : ι' → ι<GOAL>Continuous fun x => x ∘ φ
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>X : ι → Type u_8<VAR>(i : ι) → TopologicalSpace (X i)<VAR>g : (i : ι) → π i → X i<VAR>hg : ∀ (i : ι), Continuous (g i)<GOAL>Continuous fun f i => g i (f i)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>g : X → Y<VAR>hg : Continuous g<GOAL>Continuous fun x => g ∘ x
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>ι' : Type u_8<VAR>φ : ι' → ι<GOAL>TopologicalSpace.induced (fun f j => f (φ j)) Pi.topologicalSpace = ⨅ i', TopologicalSpace.induced (Function.eval (φ i')) (T (φ i'))
<VAR>Y : Type v<VAR>ι : Type u_5<VAR>TopologicalSpace Y<VAR>ι' : Type u_8<VAR>φ : ι' → ι<GOAL>TopologicalSpace.induced (fun x => x ∘ φ) Pi.topologicalSpace = ⨅ i', TopologicalSpace.induced (Function.eval (φ i')) inst✝
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>S : Set ι<GOAL>Continuous S.restrict
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>S : Set ι<GOAL>TopologicalSpace.induced S.restrict Pi.topologicalSpace = ⨅ i ∈ S, TopologicalSpace.induced (Function.eval i) (T i)
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>𝔖 : Set (Set ι)<GOAL>TopologicalSpace.induced (⋃₀ 𝔖).restrict Pi.topologicalSpace = ⨅ S ∈ 𝔖, TopologicalSpace.induced S.restrict Pi.topologicalSpace
<VAR>Y : Type v<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>DecidableEq ι<VAR>l : Filter Y<VAR>f : Y → (i : ι) → π i<VAR>x : (i : ι) → π i<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>i : ι<VAR>g : Y → π i<VAR>xi : π i<VAR>hg : Filter.Tendsto g l (𝓝 xi)<GOAL>Filter.Tendsto (fun a => Function.update (f a) i (g a)) l (𝓝 (Function.update x i xi))
<VAR>X : Type u<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>DecidableEq ι<VAR>x : X<VAR>hf : ContinuousAt f x<VAR>i : ι<VAR>g : X → π i<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (fun a => Function.update (f a) i (g a)) x
<VAR>X : Type u<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>DecidableEq ι<VAR>hf : Continuous f<VAR>i : ι<VAR>g : X → π i<VAR>hg : Continuous g<GOAL>Continuous fun a => Function.update (f a) i (g a)
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>DecidableEq ι<VAR>i : ι<GOAL>Continuous fun f => Function.update f.1 i f.2
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>(i : ι) → Zero (π i)<VAR>DecidableEq ι<VAR>i : ι<GOAL>Continuous fun x => Pi.single i x
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>(i : ι) → One (π i)<VAR>DecidableEq ι<VAR>i : ι<GOAL>Continuous fun x => Pi.mulSingle i x
<VAR>Y : Type v<VAR>n : ℕ<VAR>π : Fin (n + 1) → Type u_8<VAR>(i : Fin (n + 1)) → TopologicalSpace (π i)<VAR>i : Fin (n + 1)<VAR>f : Y → π i<VAR>l : Filter Y<VAR>x : π i<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>g : Y → (j : Fin n) → π (i.succAbove j)<VAR>y : (j : Fin n) → π (i.succAbove j)<VAR>hg : Filter.Tendsto g l (𝓝 y)<GOAL>Filter.Tendsto (fun a => i.insertNth (f a) (g a)) l (𝓝 (i.insertNth x y))
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>n : ℕ<VAR>π : Fin (n + 1) → Type u_8<VAR>(i : Fin (n + 1)) → TopologicalSpace (π i)<VAR>i : Fin (n + 1)<VAR>f : X → π i<VAR>x : X<VAR>hf : ContinuousAt f x<VAR>g : X → (j : Fin n) → π (i.succAbove j)<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (fun a => i.insertNth (f a) (g a)) x
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>n : ℕ<VAR>π : Fin (n + 1) → Type u_8<VAR>(i : Fin (n + 1)) → TopologicalSpace (π i)<VAR>i : Fin (n + 1)<VAR>f : X → π i<VAR>hf : Continuous f<VAR>g : X → (j : Fin n) → π (i.succAbove j)<VAR>hg : Continuous g<GOAL>Continuous fun a => i.insertNth (f a) (g a)
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>i : Set ι<VAR>s : (a : ι) → Set (π a)<VAR>hi : i.Finite<VAR>hs : ∀ a ∈ i, IsOpen (s a)<GOAL>IsOpen (i.pi s)
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>s : Set ((a : ι) → π a)<GOAL>IsOpen s ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>Finite ι<VAR>s : Set ((a : ι) → π a)<GOAL>IsOpen s ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ Set.univ.pi u ⊆ s
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>i : Set ι<VAR>s : (a : ι) → Set (π a)<VAR>hs : ∀ a ∈ i, IsClosed (s a)<GOAL>IsClosed (i.pi s)
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>I : Set ι<VAR>s : (i : ι) → Set (π i)<VAR>a : (i : ι) → π i<VAR>hs : I.pi s ∈ 𝓝 a<VAR>i : ι<VAR>hi : i ∈ I<GOAL>s i ∈ 𝓝 (a i)
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>i : Set ι<VAR>s : (a : ι) → Set (π a)<VAR>x : (a : ι) → π a<VAR>hi : i.Finite<VAR>hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)<GOAL>i.pi s ∈ 𝓝 x
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : (i : ι) → Set (π i)<VAR>a : (i : ι) → π i<GOAL>I.pi s ∈ 𝓝 a ↔ ∀ i ∈ I, s i ∈ 𝓝 (a i)
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : (i : ι) → Set (π i)<GOAL>interior (I.pi s) = I.pi fun i => interior (s i)
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>DecidableEq ι<VAR>s : Set ((a : ι) → π a)<VAR>x : (a : ι) → π a<VAR>hs : s ∈ 𝓝 x<VAR>y : (a : ι) → π a<GOAL>∃ I, I.piecewise x y ∈ s
<VAR>ι : Type u_5<VAR>π : ι → Type u_8<VAR>g : (a : ι) → Set (Set (π a))<GOAL>Pi.topologicalSpace = TopologicalSpace.generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<GOAL>Pi.topologicalSpace = TopologicalSpace.generateFrom {g | ∃ s i, (∀ a ∈ i, IsOpen (s a)) ∧ g = (↑i).pi s}
<VAR>ι : Type u_5<VAR>π : ι → Type u_8<VAR>g : (a : ι) → Set (Set (π a))<VAR>Finite ι<VAR>hg : ∀ (a : ι), ⋃₀ g a = Set.univ<GOAL>Pi.topologicalSpace = TopologicalSpace.generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.univ.pi s}
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>X : Type u_8<VAR>f : X → (i : ι) → π i<GOAL>TopologicalSpace.induced f Pi.topologicalSpace = ⨅ i, TopologicalSpace.induced (fun x => f x i) inferInstance
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>X : Type u_8<VAR>f : (i : ι) → X → π i<GOAL>Inducing fun x i => f i x
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>i : ι<GOAL>Continuous (Sigma.mk i)
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>s : Set (Sigma σ)<GOAL>IsOpen s ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>s : Set (Sigma σ)<GOAL>IsClosed s ↔ ∀ (i : ι), IsClosed (Sigma.mk i ⁻¹' s)
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>i : ι<GOAL>IsOpenMap (Sigma.mk i)
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>i : ι<GOAL>IsOpen (Set.range (Sigma.mk i))
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>i : ι<GOAL>IsClosedMap (Sigma.mk i)
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>i : ι<GOAL>IsClosed (Set.range (Sigma.mk i))
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>i : ι<GOAL>OpenEmbedding (Sigma.mk i)
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>i : ι<GOAL>ClosedEmbedding (Sigma.mk i)
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>i : ι<GOAL>Embedding (Sigma.mk i)
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>i : ι<VAR>x : σ i<GOAL>𝓝 ⟨i, x⟩ = Filter.map (Sigma.mk i) (𝓝 x)
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>x : Sigma σ<GOAL>𝓝 x = Filter.map (Sigma.mk x.fst) (𝓝 x.snd)
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>i : ι<VAR>x : σ i<GOAL>Filter.comap (Sigma.mk i) (𝓝 ⟨i, x⟩) = 𝓝 x
<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>s : Set ι<GOAL>IsOpen (Sigma.fst ⁻¹' s)
<VAR>X : Type u<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>TopologicalSpace X<VAR>f : Sigma σ → X<GOAL>Continuous f ↔ ∀ (i : ι), Continuous fun a => f ⟨i, a⟩
<VAR>X : Type u<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>TopologicalSpace X<VAR>f : Sigma σ → X<VAR>hf : ∀ (i : ι), Continuous fun a => f ⟨i, a⟩<GOAL>Continuous f
<VAR>X : Type u<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>TopologicalSpace X<VAR>f : Sigma σ → X<GOAL>Inducing f ↔ (∀ (i : ι), Inducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>(k : κ) → TopologicalSpace (τ k)<VAR>f₁ : ι → κ<VAR>f₂ : (i : ι) → σ i → τ (f₁ i)<GOAL>Continuous (Sigma.map f₁ f₂) ↔ ∀ (i : ι), Continuous (f₂ i)
<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>(k : κ) → TopologicalSpace (τ k)<VAR>f₁ : ι → κ<VAR>f₂ : (i : ι) → σ i → τ (f₁ i)<VAR>hf : ∀ (i : ι), Continuous (f₂ i)<GOAL>Continuous (Sigma.map f₁ f₂)
<VAR>X : Type u<VAR>ι : Type u_5<VAR>σ : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>TopologicalSpace X<VAR>f : Sigma σ → X<GOAL>IsOpenMap f ↔ ∀ (i : ι), IsOpenMap fun a => f ⟨i, a⟩
<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>(k : κ) → TopologicalSpace (τ k)<VAR>f₁ : ι → κ<VAR>f₂ : (i : ι) → σ i → τ (f₁ i)<GOAL>IsOpenMap (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsOpenMap (f₂ i)
<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>(k : κ) → TopologicalSpace (τ k)<VAR>f₁ : ι → κ<VAR>f₂ : (i : ι) → σ i → τ (f₁ i)<VAR>h₁ : Function.Injective f₁<GOAL>Inducing (Sigma.map f₁ f₂) ↔ ∀ (i : ι), Inducing (f₂ i)
<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>(k : κ) → TopologicalSpace (τ k)<VAR>f₁ : ι → κ<VAR>f₂ : (i : ι) → σ i → τ (f₁ i)<VAR>h : Function.Injective f₁<GOAL>Embedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), Embedding (f₂ i)
<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>(i : ι) → TopologicalSpace (σ i)<VAR>(k : κ) → TopologicalSpace (τ k)<VAR>f₁ : ι → κ<VAR>f₂ : (i : ι) → σ i → τ (f₁ i)<VAR>h : Function.Injective f₁<GOAL>OpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), OpenEmbedding (f₂ i)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set (ULift.{v, u} X)<GOAL>IsOpen s ↔ IsOpen (ULift.up ⁻¹' s)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set (ULift.{v, u} X)<GOAL>IsClosed s ↔ IsClosed (ULift.up ⁻¹' s)
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Continuous ULift.down
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Continuous ULift.up
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Embedding ULift.down
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>ClosedEmbedding ULift.down
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>t : Set ↑s<VAR>ht : IsOpen t<VAR>hs : IsOpen s<GOAL>IsOpen (Subtype.val '' t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>t : Set ↑s<VAR>ht : IsClosed t<VAR>hs : IsClosed s<GOAL>IsClosed (Subtype.val '' t)
<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<GOAL>𝓝ˢ (s ×ˢ t) ≤ 𝓝ˢ s ×ˢ 𝓝ˢ t
<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<VAR>p : X × Y → Prop<GOAL>(∀ᶠ (q : X × Y) in 𝓝ˢ (s ×ˢ t), p q) ↔ ∀ x ∈ s, ∀ y ∈ t, ∃ px, (∀ᶠ (x' : X) in 𝓝 x, px x') ∧ ∃ py, (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<VAR>p : X × Y → Prop<VAR>px : X → Prop<VAR>py : Y → Prop<VAR>hp : ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)<VAR>hs : ∀ᶠ (x : X) in 𝓝ˢ s, px x<VAR>ht : ∀ᶠ (y : Y) in 𝓝ˢ t, py y<GOAL>∀ᶠ (q : X × Y) in 𝓝ˢ (s ×ˢ t), p q
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<VAR>f : C^⊤⟮I, M; 𝕜⟯⟨x⟩<VAR>k : 𝕜<GOAL>f • k = f x * k
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>X : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯<VAR>f : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯<VAR>x : M<GOAL>((Derivation.evalAt x) X) f = (X f) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : C^⊤⟮I, M; I', M'⟯<VAR>x : M<VAR>v : PointDerivation I x<VAR>g : C^⊤⟮I', M'; 𝓘(𝕜, 𝕜), 𝕜⟯<GOAL>((𝒅 f x) v) g = v (g.comp f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : C^⊤⟮I, M; I', M'⟯<VAR>x : M<VAR>y : M'<VAR>h : f x = y<VAR>v : PointDerivation I x<VAR>g : C^⊤⟮I', M'; 𝓘(𝕜, 𝕜), 𝕜⟯<GOAL>((𝒅ₕ h) v) g = ((𝒅 f x) v) g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>g : C^⊤⟮I', M'; I'', M''⟯<VAR>f : C^⊤⟮I, M; I', M'⟯<VAR>x : M<GOAL>𝒅 (g.comp f) x = 𝒅 g (f x) ∘ₗ 𝒅 f x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>a : G<GOAL>⇑(Homeomorph.mulLeft a) = fun x => a * x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>a : G<GOAL>⇑(Homeomorph.addLeft a) = fun x => a + x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>a : G<GOAL>(Homeomorph.mulLeft a).symm = Homeomorph.mulLeft a⁻¹
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>a : G<GOAL>(Homeomorph.addLeft a).symm = Homeomorph.addLeft (-a)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>a : G<GOAL>IsOpenMap fun x => a * x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>a : G<GOAL>IsOpenMap fun x => a + x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>U : Set G<VAR>h : IsOpen U<VAR>x : G<GOAL>IsOpen (x +ᵥ U)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>U : Set G<VAR>h : IsOpen U<VAR>x : G<GOAL>IsOpen (x • U)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>a : G<GOAL>IsClosedMap fun x => a * x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>a : G<GOAL>IsClosedMap fun x => a + x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>U : Set G<VAR>h : IsClosed U<VAR>x : G<GOAL>IsClosed (x +ᵥ U)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>U : Set G<VAR>h : IsClosed U<VAR>x : G<GOAL>IsClosed (x • U)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>a : G<GOAL>⇑(Homeomorph.mulRight a) = fun x => x * a
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>a : G<GOAL>⇑(Homeomorph.addRight a) = fun x => x + a
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>a : G<GOAL>(Homeomorph.mulRight a).symm = Homeomorph.mulRight a⁻¹
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>a : G<GOAL>(Homeomorph.addRight a).symm = Homeomorph.addRight (-a)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>a : G<GOAL>IsOpenMap fun x => x + a
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>a : G<GOAL>IsOpenMap fun x => x * a
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>U : Set G<VAR>h : IsOpen U<VAR>x : G<GOAL>IsOpen (MulOpposite.op x • U)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>U : Set G<VAR>h : IsOpen U<VAR>x : G<GOAL>IsOpen (AddOpposite.op x +ᵥ U)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>a : G<GOAL>IsClosedMap fun x => x + a
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>a : G<GOAL>IsClosedMap fun x => x * a
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>U : Set G<VAR>h : IsClosed U<VAR>x : G<GOAL>IsClosed (MulOpposite.op x • U)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>U : Set G<VAR>h : IsClosed U<VAR>x : G<GOAL>IsClosed (AddOpposite.op x +ᵥ U)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>h : IsOpen {0}<GOAL>DiscreteTopology G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>h : IsOpen {1}<GOAL>DiscreteTopology G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<GOAL>DiscreteTopology G ↔ IsOpen {1}
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<GOAL>DiscreteTopology G ↔ IsOpen {0}
<VAR>G : Type u<VAR>TopologicalSpace G<VAR>Neg G<VAR>self : ContinuousNeg G<GOAL>Continuous fun a => -a
<VAR>G : Type u<VAR>TopologicalSpace G<VAR>Inv G<VAR>self : ContinuousInv G<GOAL>Continuous fun a => a⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>FunLike F α β<VAR>Group α<VAR>Group β<VAR>MonoidHomClass F α β<VAR>tβ : TopologicalSpace β<VAR>ContinuousInv β<VAR>f : F<GOAL>ContinuousInv α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>FunLike F α β<VAR>AddGroup α<VAR>AddGroup β<VAR>AddMonoidHomClass F α β<VAR>tβ : TopologicalSpace β<VAR>ContinuousNeg β<VAR>f : F<GOAL>ContinuousNeg α
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Neg G<VAR>ContinuousNeg G<VAR>x y : G<VAR>h : x ⤳ y<GOAL>(-x) ⤳ (-y)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Inv G<VAR>ContinuousInv G<VAR>x y : G<VAR>h : x ⤳ y<GOAL>x⁻¹ ⤳ y⁻¹
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Inv G<VAR>ContinuousInv G<VAR>x y : G<VAR>h : Inseparable x y<GOAL>Inseparable x⁻¹ y⁻¹
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Neg G<VAR>ContinuousNeg G<VAR>x y : G<VAR>h : Inseparable x y<GOAL>Inseparable (-x) (-y)
<VAR>G : Type u_1<VAR>DivInvMonoid G<VAR>TopologicalSpace G<VAR>ContinuousMul G<VAR>ContinuousInv G<VAR>x y : G<VAR>h : x ⤳ y<VAR>m : ℤ<GOAL>(x ^ m) ⤳ (y ^ m)
<VAR>G : Type u_1<VAR>SubNegMonoid G<VAR>TopologicalSpace G<VAR>ContinuousAdd G<VAR>ContinuousNeg G<VAR>x y : G<VAR>h : x ⤳ y<VAR>m : ℤ<GOAL>(m • x) ⤳ (m • y)
<VAR>G : Type u_1<VAR>SubNegMonoid G<VAR>TopologicalSpace G<VAR>ContinuousAdd G<VAR>ContinuousNeg G<VAR>x y : G<VAR>h : Inseparable x y<VAR>m : ℤ<GOAL>Inseparable (m • x) (m • y)
<VAR>G : Type u_1<VAR>DivInvMonoid G<VAR>TopologicalSpace G<VAR>ContinuousMul G<VAR>ContinuousInv G<VAR>x y : G<VAR>h : Inseparable x y<VAR>m : ℤ<GOAL>Inseparable (x ^ m) (y ^ m)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Inv G<VAR>ContinuousInv G<VAR>s : Set G<GOAL>ContinuousOn Inv.inv s
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Neg G<VAR>ContinuousNeg G<VAR>s : Set G<GOAL>ContinuousOn Neg.neg s
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Neg G<VAR>ContinuousNeg G<VAR>s : Set G<VAR>x : G<GOAL>ContinuousWithinAt Neg.neg s x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Inv G<VAR>ContinuousInv G<VAR>s : Set G<VAR>x : G<GOAL>ContinuousWithinAt Inv.inv s x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Neg G<VAR>ContinuousNeg G<VAR>x : G<GOAL>ContinuousAt Neg.neg x