ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>Zero X<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>CommSemiring R<VAR>TopologicalSemiring R<VAR>StarRing R<VAR>ContinuousStar R<VAR>f : ContinuousMapZero X R<GOAL>ContinuousMapZero.toContinuousMapHom f = ↑f
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>Zero X<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>CommSemiring R<VAR>TopologicalSemiring R<VAR>StarRing R<VAR>ContinuousStar R<GOAL>⇑ContinuousMapZero.toContinuousMapHom = toContinuousMap
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>Zero X<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>CommSemiring R<VAR>TopologicalSemiring R<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → ContinuousMapZero X R<GOAL>⇑(s.sum f) = ∑ i ∈ s, ⇑(f i)
<VAR>X : Type u_3<VAR>R : Type u_4<VAR>Zero X<VAR>TopologicalSpace X<VAR>CommRing R<VAR>TopologicalSpace R<VAR>TopologicalRing R<VAR>f : ContinuousMapZero X R<GOAL>⇑(-f) = -⇑f
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>Zero X<VAR>TopologicalSpace X<VAR>Zero R<VAR>UniformSpace R<GOAL>UniformEmbedding toContinuousMap
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>Zero X<VAR>TopologicalSpace X<VAR>Zero R<VAR>UniformSpace R<VAR>Y : Type u_3<VAR>UniformSpace Y<VAR>Zero Y<VAR>g : ContinuousMapZero Y R<VAR>hg : UniformEmbedding ⇑g<GOAL>UniformEmbedding fun x => g.comp x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>R : Type u_4<VAR>Zero X<VAR>Zero Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace R<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>f : ContinuousMapZero X Y<VAR>g : ContinuousMapZero Y R<GOAL>(ContinuousMapZero.nonUnitalStarAlgHom_precomp R f) g = g.comp f
<VAR>X : Type u_1<VAR>M : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Zero X<VAR>CommSemiring M<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>TopologicalSpace S<VAR>CommSemiring R<VAR>StarRing R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>CommSemiring S<VAR>StarRing S<VAR>TopologicalSemiring S<VAR>ContinuousStar S<VAR>Module M R<VAR>Module M S<VAR>ContinuousConstSMul M R<VAR>ContinuousConstSMul M S<VAR>φ : R →⋆ₙₐ[M] S<VAR>hφ : Continuous ⇑φ<VAR>f : ContinuousMapZero X R<GOAL>(ContinuousMapZero.nonUnitalStarAlgHom_postcomp X φ hφ) f = { toFun := ⇑φ, continuous_toFun := hφ, map_zero' := ⋯ }.comp f
<VAR>R : Type u<VAR>Ring R<VAR>Γ₀ : Type v<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<GOAL>RingSubgroupsBasis fun γ => v.ltAddSubgroup γ
<VAR>R : Type u<VAR>Ring R<VAR>Γ₀ : outParam (Type v)<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>self : Valued R Γ₀<VAR>s : Set R<GOAL>s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
<VAR>R : Type u<VAR>Ring R<VAR>Γ₀ : Type v<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<GOAL>(𝓝 0).HasBasis (fun x => True) fun γ => {x | Valued.v x < ↑γ}
<VAR>R : Type u<VAR>Ring R<VAR>Γ₀ : Type v<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<GOAL>(uniformity R).HasBasis (fun x => True) fun γ => {p | Valued.v (p.2 - p.1) < ↑γ}
<VAR>R : Type u<VAR>Ring R<VAR>Γ₀ : Type v<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<GOAL>Valued.toUniformSpace = TopologicalAddGroup.toUniformSpace R
<VAR>R : Type u<VAR>Ring R<VAR>Γ₀ : Type v<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>s : Set R<VAR>x : R<GOAL>s ∈ 𝓝 x ↔ ∃ γ, {y | Valued.v (y - x) < ↑γ} ⊆ s
<VAR>R : Type u<VAR>Ring R<VAR>Γ₀ : Type v<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>s : Set R<GOAL>s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
<VAR>R : Type u<VAR>Ring R<VAR>Γ₀ : Type v<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>x : R<VAR>h : Valued.v x ≠ 0<GOAL>{y | Valued.v y = Valued.v x} ∈ 𝓝 x
<VAR>R : Type u<VAR>Ring R<VAR>Γ₀ : Type v<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>F : Filter R<GOAL>Cauchy F ↔ F.NeBot ∧ ∀ (γ : Γ₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, Valued.v (y - x) < ↑γ
<VAR>R : Type u<VAR>Ring R<VAR>Γ₀ : Type v<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<GOAL>IsOpen ↑Valued.v.integer
<VAR>Γ₀ : Type v<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>K : Type u<VAR>Field K<VAR>hv : Valued K Γ₀<GOAL>IsOpen ↑Valued.v.valuationSubring
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>SecondCountableTopology X<GOAL>∃ f, Inducing f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T3Space X<VAR>SecondCountableTopology X<GOAL>∃ f, Embedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>[IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x}, ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>DiscreteTopology X<VAR>f : X → Y<GOAL>IsLocallyConstant f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>y : Y<GOAL>IsOpen {x | f x = y}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>y : Y<GOAL>IsClosed {x | f x = y}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>y : Y<GOAL>IsClopen {x | f x = y}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>IsLocallyConstant f ↔ ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>IsLocallyConstant f ↔ ∀ (x : X), ∀ᶠ (y : X) in 𝓝 x, f y = f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>x : X<GOAL>∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>x : X<GOAL>∀ᶠ (y : X) in 𝓝 x, f y = f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>IsLocallyConstant f ↔ ∀ (x : X), IsOpen (f ⁻¹' {f x})
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>IsLocallyConstant f ↔ ∀ (y : Y), IsOpen (f ⁻¹' {y})
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<GOAL>Continuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<GOAL>∀ {x : TopologicalSpace Y} [inst : DiscreteTopology Y] (f : X → Y), IsLocallyConstant f ↔ Continuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>h : ∀ (x y : X), f x = f y<GOAL>IsLocallyConstant f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>y : Y<GOAL>IsLocallyConstant (Function.const X y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>g : Y → Z<GOAL>IsLocallyConstant (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Y' : Type u_5<VAR>f : X → Y<VAR>f' : X → Y'<VAR>hf : IsLocallyConstant f<VAR>hf' : IsLocallyConstant f'<GOAL>IsLocallyConstant fun x => (f x, f' x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Y₁ : Type u_5<VAR>Y₂ : Type u_6<VAR>Z : Type u_7<VAR>f : X → Y₁<VAR>g : X → Y₂<VAR>hf : IsLocallyConstant f<VAR>hg : IsLocallyConstant g<VAR>h : Y₁ → Y₂ → Z<GOAL>IsLocallyConstant fun x => h (f x) (g x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>g : Y → Z<VAR>f : X → Y<VAR>hg : IsLocallyConstant g<VAR>hf : Continuous f<GOAL>IsLocallyConstant (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>x y : X<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f x = f y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>PreconnectedSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>x y : X<GOAL>f x = f y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>PreconnectedSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>x : X<GOAL>f = Function.const X (f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>PreconnectedSpace X<VAR>Nonempty Y<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<GOAL>∃ y, f = Function.const X y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>PreconnectedSpace X<VAR>f : X → Y<GOAL>IsLocallyConstant f ↔ ∀ (x y : X), f x = f y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<GOAL>(Set.range f).Finite
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Zero Y<GOAL>IsLocallyConstant 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>One Y<GOAL>IsLocallyConstant 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Neg Y<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<GOAL>IsLocallyConstant (-f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Inv Y<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<GOAL>IsLocallyConstant f⁻¹
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Add Y<VAR>f g : X → Y<VAR>hf : IsLocallyConstant f<VAR>hg : IsLocallyConstant g<GOAL>IsLocallyConstant (f + g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Mul Y<VAR>f g : X → Y<VAR>hf : IsLocallyConstant f<VAR>hg : IsLocallyConstant g<GOAL>IsLocallyConstant (f * g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Sub Y<VAR>f g : X → Y<VAR>hf : IsLocallyConstant f<VAR>hg : IsLocallyConstant g<GOAL>IsLocallyConstant (f - g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Div Y<VAR>f g : X → Y<VAR>hf : IsLocallyConstant f<VAR>hg : IsLocallyConstant g<GOAL>IsLocallyConstant (f / g)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>α : Type u_5<VAR>β : Type u_6<VAR>f : X → α<VAR>g : α → β<VAR>h : IsLocallyConstant (g ∘ f)<VAR>inj : Function.Injective g<GOAL>IsLocallyConstant f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>LocallyConnectedSpace X<VAR>f : X → Y<VAR>h : ∀ (x y : X), y ∈ connectedComponent x → f y = f x<GOAL>IsLocallyConstant f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>LocallyConnectedSpace X<VAR>f : X → Y<VAR>h : ∀ (U : Set X), IsConnected U → IsClopen U → ∀ x ∈ U, ∀ y ∈ U, f y = f x<GOAL>IsLocallyConstant f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>LocallyConnectedSpace X<VAR>f : X → Y<VAR>h : ∀ (U : Set X), IsPreconnected U → IsClopen U → ∀ x ∈ U, ∀ y ∈ U, f y = f x<GOAL>IsLocallyConstant f
<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>TopologicalSpace X<VAR>self : LocallyConstant X Y<GOAL>IsLocallyConstant self.toFun
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : LocallyConstant X Y<GOAL>f.toFun = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>h : IsLocallyConstant f<GOAL>⇑{ toFun := f, isLocallyConstant := h } = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f g : LocallyConstant X Y<VAR>h : f = g<VAR>x : X<GOAL>f x = g x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : LocallyConstant X Y<VAR>x y : X<VAR>h : x = y<GOAL>f x = f y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<GOAL>Function.Injective DFunLike.coe
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f g : LocallyConstant X Y<GOAL>⇑f = ⇑g ↔ f = g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f g : LocallyConstant X Y<VAR>h : ∀ (x : X), f x = g x<GOAL>f = g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f g : LocallyConstant X Y<GOAL>f = g ↔ ∀ (x : X), f x = g x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : LocallyConstant X Y<GOAL>Continuous ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : LocallyConstant X Y<GOAL>⇑↑f = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Function.Injective LocallyConstant.toContinuousMap
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>y : Y<GOAL>⇑(LocallyConstant.const X y) = Function.const X y
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>U : Set X<VAR>(x : X) → Decidable (x ∈ U)<VAR>hU : IsClopen U<GOAL>⇑(LocallyConstant.ofIsClopen hU) ⁻¹' {0} = U
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>U : Set X<VAR>(x : X) → Decidable (x ∈ U)<VAR>hU : IsClopen U<GOAL>⇑(LocallyConstant.ofIsClopen hU) ⁻¹' {1} = Uᶜ
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>f g : LocallyConstant X (Fin 2)<VAR>h : ⇑f ⁻¹' {0} = ⇑g ⁻¹' {0}<GOAL>f = g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>f : LocallyConstant X Y<GOAL>(Set.range ⇑f).Finite
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : LocallyConstant X Y<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>x y : X<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f x = f y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>PreconnectedSpace X<VAR>f : LocallyConstant X Y<VAR>x y : X<GOAL>f x = f y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>PreconnectedSpace X<VAR>f : LocallyConstant X Y<VAR>x : X<GOAL>f = LocallyConstant.const X (f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>PreconnectedSpace X<VAR>Nonempty Y<VAR>f : LocallyConstant X Y<GOAL>∃ y, f = LocallyConstant.const X y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>f : Y → Z<VAR>g : LocallyConstant X Y<GOAL>⇑(LocallyConstant.map f g) = f ∘ ⇑g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<GOAL>LocallyConstant.map id = id
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Y₁ : Type u_5<VAR>Y₂ : Type u_6<VAR>Y₃ : Type u_7<VAR>g : Y₂ → Y₃<VAR>f : Y₁ → Y₂<GOAL>LocallyConstant.map g ∘ LocallyConstant.map f = LocallyConstant.map (g ∘ f)
<VAR>X : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Finite α<VAR>TopologicalSpace X<VAR>f : LocallyConstant X (α → β)<GOAL>LocallyConstant.unflip f.flip = f
<VAR>X : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Finite α<VAR>TopologicalSpace X<VAR>f : α → LocallyConstant X β<GOAL>(LocallyConstant.unflip f).flip = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>g : LocallyConstant Y Z<GOAL>⇑(LocallyConstant.comap f g) = ⇑g ∘ ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>g : LocallyConstant Y Z<VAR>x : X<GOAL>(LocallyConstant.comap f g) x = g (f x)
<VAR>X : Type u_1<VAR>Z : Type u_3<VAR>TopologicalSpace X<GOAL>LocallyConstant.comap (ContinuousMap.id X) = id
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>W : Type u_5<VAR>TopologicalSpace W<VAR>f : C(W, X)<VAR>g : C(X, Y)<GOAL>LocallyConstant.comap (g.comp f) = LocallyConstant.comap f ∘ LocallyConstant.comap g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>W : Type u_5<VAR>TopologicalSpace W<VAR>f : C(W, X)<VAR>g : C(X, Y)<VAR>x : LocallyConstant Y Z<GOAL>LocallyConstant.comap f (LocallyConstant.comap g x) = LocallyConstant.comap (g.comp f) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>y : Y<VAR>h : ∀ (x : X), f x = y<GOAL>LocallyConstant.comap f = fun g => LocallyConstant.const X (g y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>hfs : Function.Surjective f.toFun<GOAL>Function.Injective (LocallyConstant.comap f)
<VAR>X : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>TopologicalSpace X<VAR>f : X → α<VAR>g : α → β<VAR>h : LocallyConstant X β<VAR>cond : g ∘ f = ⇑h<VAR>inj : Function.Injective g<GOAL>⇑(LocallyConstant.desc f h cond inj) = f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R : Type u_5<VAR>One R<VAR>U : Set X<VAR>f : LocallyConstant X R<VAR>hU : IsClopen U<VAR>x : X<GOAL>(f.mulIndicator hU) x = U.mulIndicator (⇑f) x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R : Type u_5<VAR>Zero R<VAR>U : Set X<VAR>f : LocallyConstant X R<VAR>hU : IsClopen U<VAR>x : X<GOAL>(f.indicator hU) x = U.indicator (⇑f) x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R : Type u_5<VAR>One R<VAR>U : Set X<VAR>f : LocallyConstant X R<VAR>a : X<VAR>hU : IsClopen U<GOAL>(f.mulIndicator hU) a = if a ∈ U then f a else 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R : Type u_5<VAR>Zero R<VAR>U : Set X<VAR>f : LocallyConstant X R<VAR>a : X<VAR>hU : IsClopen U<GOAL>(f.indicator hU) a = if a ∈ U then f a else 0
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R : Type u_5<VAR>One R<VAR>U : Set X<VAR>f : LocallyConstant X R<VAR>a : X<VAR>hU : IsClopen U<VAR>h : a ∈ U<GOAL>(f.mulIndicator hU) a = f a
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R : Type u_5<VAR>Zero R<VAR>U : Set X<VAR>f : LocallyConstant X R<VAR>a : X<VAR>hU : IsClopen U<VAR>h : a ∈ U<GOAL>(f.indicator hU) a = f a
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R : Type u_5<VAR>One R<VAR>U : Set X<VAR>f : LocallyConstant X R<VAR>a : X<VAR>hU : IsClopen U<VAR>h : a ∉ U<GOAL>(f.mulIndicator hU) a = 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R : Type u_5<VAR>Zero R<VAR>U : Set X<VAR>f : LocallyConstant X R<VAR>a : X<VAR>hU : IsClopen U<VAR>h : a ∉ U<GOAL>(f.indicator hU) a = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<VAR>g : LocallyConstant X Z<GOAL>(LocallyConstant.congrLeft e) g = LocallyConstant.comap e.symm.toContinuousMap g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<VAR>g : LocallyConstant Y Z<GOAL>(LocallyConstant.congrLeft e).symm g = LocallyConstant.comap e.toContinuousMap g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>e : Y ≃ Z<VAR>g : LocallyConstant X Z<GOAL>(LocallyConstant.congrRight e).symm g = LocallyConstant.map (⇑e.symm) g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>e : Y ≃ Z<VAR>g : LocallyConstant X Y<GOAL>(LocallyConstant.congrRight e) g = LocallyConstant.map (⇑e) g
<VAR>X : Type u_1<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>C₁ C₂ : Set X<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>h : C₁ ∪ C₂ = Set.univ<VAR>f : LocallyConstant (↑C₁) Z<VAR>g : LocallyConstant (↑C₂) Z<VAR>hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩<VAR>DecidablePred fun x => x ∈ C₁<VAR>x : X<VAR>hx : x ∈ C₁<GOAL>(LocallyConstant.piecewise h₁ h₂ h f g hfg) x = f ⟨x, hx⟩
<VAR>X : Type u_1<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>C₁ C₂ : Set X<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>h : C₁ ∪ C₂ = Set.univ<VAR>f : LocallyConstant (↑C₁) Z<VAR>g : LocallyConstant (↑C₂) Z<VAR>hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩<VAR>DecidablePred fun x => x ∈ C₁<VAR>x : X<VAR>hx : x ∈ C₂<GOAL>(LocallyConstant.piecewise h₁ h₂ h f g hfg) x = g ⟨x, hx⟩
<VAR>X : Type u_1<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>C₀ C₁ C₂ : Set X<VAR>h₀ : C₀ ⊆ C₁ ∪ C₂<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>f₁ : LocallyConstant (↑C₁) Z<VAR>f₂ : LocallyConstant (↑C₂) Z<VAR>DecidablePred fun x => x ∈ C₁<VAR>hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩<VAR>x : ↑C₀<VAR>hx : ↑x ∈ C₁<GOAL>(LocallyConstant.piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₁ ⟨↑x, hx⟩
<VAR>X : Type u_1<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>C₀ C₁ C₂ : Set X<VAR>h₀ : C₀ ⊆ C₁ ∪ C₂<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>f₁ : LocallyConstant (↑C₁) Z<VAR>f₂ : LocallyConstant (↑C₂) Z<VAR>DecidablePred fun x => x ∈ C₁<VAR>hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩<VAR>x : ↑C₀<VAR>hx : ↑x ∈ C₂<GOAL>(LocallyConstant.piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₂ ⟨↑x, hx⟩
<VAR>G : Type u_2<VAR>TopologicalSpace G<VAR>LinearOrderedAddCommGroup G<VAR>OrderTopology G<GOAL>Continuous abs
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>TopologicalSpace G<VAR>LinearOrderedAddCommGroup G<VAR>OrderTopology G<VAR>l : Filter α<VAR>f : α → G<VAR>a : G<VAR>h : Filter.Tendsto f l (𝓝 a)<GOAL>Filter.Tendsto (fun x => |f x|) l (𝓝 |a|)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>TopologicalSpace G<VAR>LinearOrderedAddCommGroup G<VAR>OrderTopology G<VAR>l : Filter α<VAR>f : α → G<GOAL>Filter.Tendsto f l (𝓝 0) ↔ Filter.Tendsto (abs ∘ f) l (𝓝 0)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>TopologicalSpace G<VAR>LinearOrderedAddCommGroup G<VAR>OrderTopology G<VAR>f : α → G<VAR>TopologicalSpace α<VAR>h : Continuous f<GOAL>Continuous fun x => |f x|
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>TopologicalSpace G<VAR>LinearOrderedAddCommGroup G<VAR>OrderTopology G<VAR>f : α → G<VAR>TopologicalSpace α<VAR>a : α<VAR>h : ContinuousAt f a<GOAL>ContinuousAt (fun x => |f x|) a
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>TopologicalSpace G<VAR>LinearOrderedAddCommGroup G<VAR>OrderTopology G<VAR>f : α → G<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>h : ContinuousWithinAt f s a<GOAL>ContinuousWithinAt (fun x => |f x|) s a
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>TopologicalSpace G<VAR>LinearOrderedAddCommGroup G<VAR>OrderTopology G<VAR>f : α → G<VAR>TopologicalSpace α<VAR>s : Set α<VAR>h : ContinuousOn f s<GOAL>ContinuousOn (fun x => |f x|) s
<VAR>G : Type u_2<VAR>TopologicalSpace G<VAR>LinearOrderedAddCommGroup G<VAR>OrderTopology G<GOAL>Filter.Tendsto abs (𝓝[≠] 0) (𝓝[>] 0)
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>Filter.Tendsto Int.floor Filter.atTop Filter.atTop
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>Filter.Tendsto Int.floor Filter.atBot Filter.atBot
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>Filter.Tendsto Int.ceil Filter.atTop Filter.atTop
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<GOAL>Filter.Tendsto Int.ceil Filter.atBot Filter.atBot
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>n : ℤ<GOAL>ContinuousOn (fun x => ↑⌊x⌋) (Set.Ico (↑n) (↑n + 1))
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>n : ℤ<GOAL>ContinuousOn (fun x => ↑⌈x⌉) (Set.Ioc (↑n - 1) ↑n)
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>x : α<GOAL>Filter.Tendsto Int.floor (𝓝[≥] x) (pure ⌊x⌋)
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>n : ℤ<GOAL>Filter.Tendsto Int.floor (𝓝[≥] ↑n) (pure n)
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>x : α<GOAL>Filter.Tendsto Int.ceil (𝓝[≤] x) (pure ⌈x⌉)
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>n : ℤ<GOAL>Filter.Tendsto Int.ceil (𝓝[≤] ↑n) (pure n)
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>x : α<GOAL>Filter.Tendsto Int.floor (𝓝[<] x) (pure (⌈x⌉ - 1))
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>n : ℤ<GOAL>Filter.Tendsto Int.floor (𝓝[<] ↑n) (pure (n - 1))
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>x : α<GOAL>Filter.Tendsto Int.ceil (𝓝[>] x) (pure (⌊x⌋ + 1))
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>n : ℤ<GOAL>Filter.Tendsto Int.ceil (𝓝[>] ↑n) (pure (n + 1))
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>n : ℤ<GOAL>Filter.Tendsto (fun x => ↑⌊x⌋) (𝓝[≥] ↑n) (𝓝[≥] ↑n)
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>n : ℤ<GOAL>Filter.Tendsto (fun x => ↑⌊x⌋) (𝓝[≥] ↑n) (𝓝 ↑n)
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>n : ℤ<GOAL>Filter.Tendsto (fun x => ↑⌈x⌉) (𝓝[≤] ↑n) (𝓝[≤] ↑n)
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>n : ℤ<GOAL>Filter.Tendsto (fun x => ↑⌈x⌉) (𝓝[≤] ↑n) (𝓝 ↑n)
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>n : ℤ<GOAL>Filter.Tendsto (fun x => ↑⌊x⌋) (𝓝[<] ↑n) (𝓝[≤] (↑n - 1))
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>n : ℤ<GOAL>Filter.Tendsto (fun x => ↑⌈x⌉) (𝓝[>] ↑n) (𝓝[≥] (↑n + 1))
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>FloorRing α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>n : ℤ<GOAL>Filter.Tendsto (fun x => ↑⌊x⌋) (𝓝[<] ↑n) (𝓝 (↑n - 1))