ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>AddGroup G<VAR>AddAction G X<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>h_proper : ProperVAdd G X<VAR>T2Space G<GOAL>T2Space X
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>H : Type u_5<VAR>Group H<VAR>MulAction H X<VAR>TopologicalSpace H<VAR>ProperSMul G X<VAR>f : H →* G<VAR>f_clemb : ClosedEmbedding ⇑f<VAR>f_compat : ∀ (h : H) (x : X), f h • x = h • x<GOAL>ProperSMul H X
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>AddGroup G<VAR>AddAction G X<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>H : Type u_5<VAR>AddGroup H<VAR>AddAction H X<VAR>TopologicalSpace H<VAR>ProperVAdd G X<VAR>f : H →+ G<VAR>f_clemb : ClosedEmbedding ⇑f<VAR>f_compat : ∀ (h : H) (x : X), f h +ᵥ x = h +ᵥ x<GOAL>ProperVAdd H X
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>T2Space X<VAR>DiscreteTopology G<VAR>ContinuousConstSMul G X<VAR>compactlyGenerated : ∀ (s : Set (X × X)), IsClosed s ↔ ∀ ⦃K : Set (X × X)⦄, IsCompact K → IsClosed (s ∩ K)<GOAL>ProperlyDiscontinuousSMul G X ↔ ProperSMul G X
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>T2Space X<VAR>WeaklyLocallyCompactSpace X<VAR>DiscreteTopology G<VAR>ContinuousConstSMul G X<GOAL>ProperlyDiscontinuousSMul G X ↔ ProperSMul G X
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>T2Space X<VAR>FirstCountableTopology X<VAR>DiscreteTopology G<VAR>ContinuousConstSMul G X<GOAL>ProperlyDiscontinuousSMul G X ↔ ProperSMul G X
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>DivInvMonoid G₀<VAR>TopologicalSpace G₀<VAR>ContinuousMul G₀<VAR>f : α → G₀<VAR>l : Filter α<VAR>x : G₀<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>y : G₀<GOAL>Filter.Tendsto (fun a => f a / y) l (𝓝 (x / y))
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>DivInvMonoid G₀<VAR>TopologicalSpace G₀<VAR>ContinuousMul G₀<VAR>f : α → G₀<VAR>TopologicalSpace α<VAR>a : α<VAR>hf : ContinuousAt f a<VAR>y : G₀<GOAL>ContinuousAt (fun x => f x / y) a
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>DivInvMonoid G₀<VAR>TopologicalSpace G₀<VAR>ContinuousMul G₀<VAR>f : α → G₀<VAR>s : Set α<VAR>TopologicalSpace α<VAR>a : α<VAR>hf : ContinuousWithinAt f s a<VAR>y : G₀<GOAL>ContinuousWithinAt (fun x => f x / y) s a
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>DivInvMonoid G₀<VAR>TopologicalSpace G₀<VAR>ContinuousMul G₀<VAR>f : α → G₀<VAR>s : Set α<VAR>TopologicalSpace α<VAR>hf : ContinuousOn f s<VAR>y : G₀<GOAL>ContinuousOn (fun x => f x / y) s
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>DivInvMonoid G₀<VAR>TopologicalSpace G₀<VAR>ContinuousMul G₀<VAR>f : α → G₀<VAR>TopologicalSpace α<VAR>hf : Continuous f<VAR>y : G₀<GOAL>Continuous fun x => f x / y
<VAR>G₀ : Type u_4<VAR>Zero G₀<VAR>Inv G₀<VAR>TopologicalSpace G₀<VAR>self : HasContinuousInv₀ G₀<VAR>x : G₀<GOAL>x ≠ 0 → ContinuousAt Inv.inv x
<VAR>G₀ : Type u_3<VAR>Zero G₀<VAR>Inv G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>x : G₀<VAR>hx : x ≠ 0<GOAL>Filter.Tendsto Inv.inv (𝓝 x) (𝓝 x⁻¹)
<VAR>G₀ : Type u_3<VAR>Zero G₀<VAR>Inv G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<GOAL>ContinuousOn Inv.inv {0}ᶜ
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>Zero G₀<VAR>Inv G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>l : Filter α<VAR>f : α → G₀<VAR>a : G₀<VAR>hf : Filter.Tendsto f l (𝓝 a)<VAR>ha : a ≠ 0<GOAL>Filter.Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>Zero G₀<VAR>Inv G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>f : α → G₀<VAR>s : Set α<VAR>a : α<VAR>TopologicalSpace α<VAR>hf : ContinuousWithinAt f s a<VAR>ha : f a ≠ 0<GOAL>ContinuousWithinAt (fun x => (f x)⁻¹) s a
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>Zero G₀<VAR>Inv G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>f : α → G₀<VAR>a : α<VAR>TopologicalSpace α<VAR>hf : ContinuousAt f a<VAR>ha : f a ≠ 0<GOAL>ContinuousAt (fun x => (f x)⁻¹) a
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>Zero G₀<VAR>Inv G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>f : α → G₀<VAR>TopologicalSpace α<VAR>hf : Continuous f<VAR>h0 : ∀ (x : α), f x ≠ 0<GOAL>Continuous fun x => (f x)⁻¹
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>Zero G₀<VAR>Inv G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>f : α → G₀<VAR>s : Set α<VAR>TopologicalSpace α<VAR>hf : ContinuousOn f s<VAR>h0 : ∀ x ∈ s, f x ≠ 0<GOAL>ContinuousOn (fun x => (f x)⁻¹) s
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<GOAL>Embedding Units.val
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>x : G₀<VAR>hx : x ≠ 0<GOAL>𝓝 x⁻¹ = (𝓝 x)⁻¹
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>x : G₀<VAR>l : Filter α<VAR>f : α → G₀<VAR>hx : x ≠ 0<GOAL>Filter.Tendsto (fun x => (f x)⁻¹) l (𝓝 x⁻¹) ↔ Filter.Tendsto f l (𝓝 x)
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>f g : α → G₀<VAR>l : Filter α<VAR>a b : G₀<VAR>hf : Filter.Tendsto f l (𝓝 a)<VAR>hg : Filter.Tendsto g l (𝓝 b)<VAR>hy : b ≠ 0<GOAL>Filter.Tendsto (f / g) l (𝓝 (a / b))
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>T1Space G₀<VAR>f g : α → G₀<VAR>l : Filter α<VAR>x y : G₀<VAR>hg : Filter.Tendsto g l (𝓝 y)<VAR>hy : y ≠ 0<GOAL>Filter.Tendsto (fun n => f n * g n) l (𝓝 (x * y)) ↔ Filter.Tendsto f l (𝓝 x)
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>f g : α → G₀<VAR>TopologicalSpace α<VAR>s : Set α<VAR>a : α<VAR>hf : ContinuousWithinAt f s a<VAR>hg : ContinuousWithinAt g s a<VAR>h₀ : g a ≠ 0<GOAL>ContinuousWithinAt (f / g) s a
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>f g : α → G₀<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<VAR>h₀ : ∀ x ∈ s, g x ≠ 0<GOAL>ContinuousOn (f / g) s
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>f g : α → G₀<VAR>TopologicalSpace α<VAR>a : α<VAR>hf : ContinuousAt f a<VAR>hg : ContinuousAt g a<VAR>h₀ : g a ≠ 0<GOAL>ContinuousAt (f / g) a
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>f g : α → G₀<VAR>TopologicalSpace α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h₀ : ∀ (x : α), g x ≠ 0<GOAL>Continuous (f / g)
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<GOAL>ContinuousOn (fun p => p.1 / p.2) {p | p.2 ≠ 0}
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>f g : α → G₀<VAR>TopologicalSpace α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h₀ : ∀ (x : α), g x ≠ 0<GOAL>Continuous fun x => f x / g x
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>f g : α → G₀<VAR>TopologicalSpace α<VAR>a : α<VAR>hf : ContinuousAt f a<VAR>hg : ContinuousAt g a<VAR>h₀ : g a ≠ 0<GOAL>ContinuousAt (fun x => f x / g x) a
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>f g : α → G₀<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<VAR>h₀ : ∀ x ∈ s, g x ≠ 0<GOAL>ContinuousOn (fun x => f x / g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>a : α<VAR>f g : α → G₀<VAR>h : α → G₀ → β<VAR>hf : ContinuousAt f a<VAR>hg : ContinuousAt g a<VAR>hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)<VAR>h2h : g a = 0 → Filter.Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))<GOAL>ContinuousAt (fun x => h x (f x / g x)) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f g : α → G₀<VAR>h : α → G₀ → β<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hh : ∀ (a : α), g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)<VAR>h2h : ∀ (a : α), g a = 0 → Filter.Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))<GOAL>Continuous fun x => h x (f x / g x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>GroupWithZero α<VAR>ContinuousMul α<VAR>c : α<VAR>hc : c ≠ 0<GOAL>⇑(Homeomorph.mulLeft₀ c hc) = fun x => c * x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>GroupWithZero α<VAR>ContinuousMul α<VAR>c : α<VAR>hc : c ≠ 0<GOAL>⇑(Homeomorph.mulLeft₀ c hc).symm = fun x => c⁻¹ * x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>GroupWithZero α<VAR>ContinuousMul α<VAR>c : α<VAR>hc : c ≠ 0<GOAL>⇑(Homeomorph.mulRight₀ c hc) = fun x => x * c
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>GroupWithZero α<VAR>ContinuousMul α<VAR>c : α<VAR>hc : c ≠ 0<GOAL>⇑(Homeomorph.mulRight₀ c hc).symm = fun x => x * c⁻¹
<VAR>G₀ : Type u_3<VAR>TopologicalSpace G₀<VAR>GroupWithZero G₀<VAR>ContinuousMul G₀<VAR>a : G₀<VAR>ha : a ≠ 0<VAR>b : G₀<GOAL>Filter.map (fun x => a * x) (𝓝 b) = 𝓝 (a * b)
<VAR>G₀ : Type u_3<VAR>TopologicalSpace G₀<VAR>GroupWithZero G₀<VAR>ContinuousMul G₀<VAR>a : G₀<VAR>ha : a ≠ 0<GOAL>Filter.map (fun x => a * x) (𝓝 1) = 𝓝 a
<VAR>G₀ : Type u_3<VAR>TopologicalSpace G₀<VAR>GroupWithZero G₀<VAR>ContinuousMul G₀<VAR>a : G₀<VAR>ha : a ≠ 0<VAR>b : G₀<GOAL>Filter.map (fun x => x * a) (𝓝 b) = 𝓝 (b * a)
<VAR>G₀ : Type u_3<VAR>TopologicalSpace G₀<VAR>GroupWithZero G₀<VAR>ContinuousMul G₀<VAR>a : G₀<VAR>ha : a ≠ 0<GOAL>Filter.map (fun x => x * a) (𝓝 1) = 𝓝 a
<VAR>G₀ : Type u_3<VAR>TopologicalSpace G₀<VAR>GroupWithZero G₀<VAR>ContinuousMul G₀<VAR>a : G₀<VAR>ha : a ≠ 0<GOAL>Filter.comap (fun x => x * a⁻¹) (𝓝 1) = 𝓝 a
<VAR>G₀ : Type u_3<VAR>TopologicalSpace G₀<VAR>GroupWithZero G₀<VAR>ContinuousMul G₀<VAR>h : Filter.Tendsto Inv.inv (𝓝 1) (𝓝 1)<GOAL>HasContinuousInv₀ G₀
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>x : G₀<VAR>m : ℤ<VAR>h : x ≠ 0 ∨ 0 ≤ m<GOAL>ContinuousAt (fun x => x ^ m) x
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>m : ℤ<GOAL>ContinuousOn (fun x => x ^ m) {0}ᶜ
<VAR>α : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>f : α → G₀<VAR>l : Filter α<VAR>a : G₀<VAR>hf : Filter.Tendsto f l (𝓝 a)<VAR>m : ℤ<VAR>h : a ≠ 0 ∨ 0 ≤ m<GOAL>Filter.Tendsto (fun x => f x ^ m) l (𝓝 (a ^ m))
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>a : X<VAR>f : X → G₀<VAR>hf : ContinuousAt f a<VAR>m : ℤ<VAR>h : f a ≠ 0 ∨ 0 ≤ m<GOAL>ContinuousAt (fun x => f x ^ m) a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>a : X<VAR>s : Set X<VAR>f : X → G₀<VAR>hf : ContinuousWithinAt f s a<VAR>m : ℤ<VAR>h : f a ≠ 0 ∨ 0 ≤ m<GOAL>ContinuousWithinAt (fun x => f x ^ m) s a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : X → G₀<VAR>hf : ContinuousOn f s<VAR>m : ℤ<VAR>h : ∀ a ∈ s, f a ≠ 0 ∨ 0 ≤ m<GOAL>ContinuousOn (fun x => f x ^ m) s
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>TopologicalSpace G₀<VAR>HasContinuousInv₀ G₀<VAR>ContinuousMul G₀<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : X → G₀<VAR>hf : Continuous f<VAR>m : ℤ<VAR>h0 : ∀ (a : X), f a ≠ 0 ∨ 0 ≤ m<GOAL>Continuous fun x => f x ^ m
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>F : Filter X<VAR>x : X<VAR>h : AccPt x F<VAR>f : X → β<VAR>hf1 : ContinuousAt f x<VAR>hf2 : Function.Injective f<GOAL>AccPt (f x) (Filter.map f F)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>A : Set X<VAR>x : X<GOAL>x ∈ derivedSet A ↔ AccPt x (𝓟 A)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>A B : Set X<GOAL>derivedSet (A ∪ B) = derivedSet A ∪ derivedSet B
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>A B : Set X<VAR>h : A ⊆ B<GOAL>derivedSet A ⊆ derivedSet B
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>A : Set X<VAR>f : X → β<VAR>hf1 : Continuous f<VAR>hf2 : Function.Injective f<GOAL>f '' derivedSet A ⊆ derivedSet (f '' A)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>A : Set X<GOAL>derivedSet A ⊆ closure A
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>A : Set X<GOAL>IsClosed A ↔ derivedSet A ⊆ A
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>A : Set X<GOAL>derivedSet (closure A) = derivedSet A
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>A : Set X<GOAL>IsClosed (derivedSet A)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>U : Set X<GOAL>Preperfect U ↔ U ⊆ derivedSet U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>U : Set X<GOAL>Perfect U ↔ U = derivedSet U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>U : Set X<VAR>hs : IsPreconnected U<VAR>a b : Set X<VAR>h : U ⊆ a ∪ b<VAR>ha : (U ∩ derivedSet a).Nonempty<VAR>hb : (U ∩ derivedSet b).Nonempty<GOAL>(U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>AddAction G X<VAR>SigmaCompactSpace G<VAR>BaireSpace X<VAR>T2Space X<VAR>ContinuousVAdd G X<VAR>AddAction.IsPretransitive G X<VAR>U : Set G<VAR>hU : U ∈ 𝓝 0<VAR>x : X<GOAL>U +ᵥ {x} ∈ 𝓝 x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>Group G<VAR>TopologicalGroup G<VAR>MulAction G X<VAR>SigmaCompactSpace G<VAR>BaireSpace X<VAR>T2Space X<VAR>ContinuousSMul G X<VAR>MulAction.IsPretransitive G X<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>x : X<GOAL>U • {x} ∈ 𝓝 x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>AddAction G X<VAR>SigmaCompactSpace G<VAR>BaireSpace X<VAR>T2Space X<VAR>ContinuousVAdd G X<VAR>AddAction.IsPretransitive G X<VAR>x : X<GOAL>IsOpenMap fun g => g +ᵥ x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>Group G<VAR>TopologicalGroup G<VAR>MulAction G X<VAR>SigmaCompactSpace G<VAR>BaireSpace X<VAR>T2Space X<VAR>ContinuousSMul G X<VAR>MulAction.IsPretransitive G X<VAR>x : X<GOAL>IsOpenMap fun g => g • x
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>SigmaCompactSpace G<VAR>H : Type u_3<VAR>Group H<VAR>TopologicalSpace H<VAR>BaireSpace H<VAR>T2Space H<VAR>ContinuousMul H<VAR>f : G →* H<VAR>hf : Function.Surjective ⇑f<VAR>h'f : Continuous ⇑f<GOAL>IsOpenMap ⇑f
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>SigmaCompactSpace G<VAR>H : Type u_3<VAR>AddGroup H<VAR>TopologicalSpace H<VAR>BaireSpace H<VAR>T2Space H<VAR>ContinuousAdd H<VAR>f : G →+ H<VAR>hf : Function.Surjective ⇑f<VAR>h'f : Continuous ⇑f<GOAL>IsOpenMap ⇑f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>self : P →ᴬ[R] Q<GOAL>Continuous self.toFun
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f g : P →ᴬ[R] Q<VAR>h : f.toAffineMap = g.toAffineMap<GOAL>f = g
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f : P →ᴬ[R] Q<GOAL>f.toFun = ⇑f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<GOAL>Function.Injective DFunLike.coe
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f g : P →ᴬ[R] Q<VAR>h : ∀ (x : P), f x = g x<GOAL>f = g
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f g : P →ᴬ[R] Q<GOAL>f = g ↔ ∀ (x : P), f x = g x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f g : P →ᴬ[R] Q<VAR>h : f = g<VAR>x : P<GOAL>f x = g x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f : P →ᴬ[R] Q<GOAL>f.toContinuousMap = ↑f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f : P →ᴬ[R] Q<GOAL>⇑f.toAffineMap = ⇑f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f : P →ᴬ[R] Q<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f g : P →ᴬ[R] Q<VAR>h : ↑f = ↑g<GOAL>f = g
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f : P →ᵃ[R] Q<VAR>h : Continuous f.toFun<GOAL>{ toAffineMap := f, cont := h }.toAffineMap = f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f : P →ᵃ[R] Q<VAR>h : Continuous f.toFun<GOAL>↑{ toAffineMap := f, cont := h } = { toFun := ⇑f, continuous_toFun := h }
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f : P →ᵃ[R] Q<VAR>h : Continuous f.toFun<GOAL>⇑{ toAffineMap := f, cont := h } = ⇑f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f : P →ᴬ[R] Q<VAR>h : Continuous f.toFun<GOAL>{ toAffineMap := f.toAffineMap, cont := h } = f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>f : P →ᴬ[R] Q<GOAL>Continuous ⇑f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>q : Q<GOAL>⇑(ContinuousAffineMap.const R P q) = Function.const P q
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>W₂ : Type u_6<VAR>Q₂ : Type u_7<VAR>AddCommGroup W₂<VAR>Module R W₂<VAR>TopologicalSpace Q₂<VAR>AddTorsor W₂ Q₂<VAR>f : Q →ᴬ[R] Q₂<VAR>g : P →ᴬ[R] Q<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace Q<VAR>AddTorsor W Q<VAR>W₂ : Type u_6<VAR>Q₂ : Type u_7<VAR>AddCommGroup W₂<VAR>Module R W₂<VAR>TopologicalSpace Q₂<VAR>AddTorsor W₂ Q₂<VAR>f : Q →ᴬ[R] Q₂<VAR>g : P →ᴬ[R] Q<VAR>x : P<GOAL>(f.comp g) x = f (g x)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace W<GOAL>⇑0 = 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace W<VAR>x : P<GOAL>0 x = 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>S : Type u_8<VAR>TopologicalSpace W<VAR>Monoid S<VAR>DistribMulAction S W<VAR>SMulCommClass R S W<VAR>ContinuousConstSMul S W<VAR>t : S<VAR>f : P →ᴬ[R] W<GOAL>⇑(t • f) = t • ⇑f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>S : Type u_8<VAR>TopologicalSpace W<VAR>Monoid S<VAR>DistribMulAction S W<VAR>SMulCommClass R S W<VAR>ContinuousConstSMul S W<VAR>t : S<VAR>f : P →ᴬ[R] W<VAR>x : P<GOAL>(t • f) x = t • f x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace W<VAR>TopologicalAddGroup W<VAR>f g : P →ᴬ[R] W<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace W<VAR>TopologicalAddGroup W<VAR>f g : P →ᴬ[R] W<VAR>x : P<GOAL>(f + g) x = f x + g x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace W<VAR>TopologicalAddGroup W<VAR>f g : P →ᴬ[R] W<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace W<VAR>TopologicalAddGroup W<VAR>f g : P →ᴬ[R] W<VAR>x : P<GOAL>(f - g) x = f x - g x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace W<VAR>TopologicalAddGroup W<VAR>f : P →ᴬ[R] W<GOAL>⇑(-f) = -⇑f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace W<VAR>TopologicalAddGroup W<VAR>f : P →ᴬ[R] W<VAR>x : P<GOAL>(-f) x = -f x