ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : ℕ → Type u_1<VAR>x y z : (n : ℕ) → E n<VAR>h : x ≠ z<GOAL>min (PiNat.firstDiff x y) (PiNat.firstDiff y z) ≤ PiNat.firstDiff x z
<VAR>E : ℕ → Type u_1<VAR>x : (n : ℕ) → E n<VAR>n : ℕ<GOAL>PiNat.cylinder x n = (↑(Finset.range n)).pi fun i => {x i}
<VAR>E : ℕ → Type u_1<VAR>x : (n : ℕ) → E n<GOAL>PiNat.cylinder x 0 = Set.univ
<VAR>E : ℕ → Type u_1<VAR>x : (n : ℕ) → E n<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>PiNat.cylinder x n ⊆ PiNat.cylinder x m
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<GOAL>y ∈ PiNat.cylinder x n ↔ ∀ i < n, y i = x i
<VAR>E : ℕ → Type u_1<VAR>x : (n : ℕ) → E n<VAR>n : ℕ<GOAL>x ∈ PiNat.cylinder x n
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<GOAL>y ∈ PiNat.cylinder x n ↔ PiNat.cylinder y n = PiNat.cylinder x n
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<GOAL>y ∈ PiNat.cylinder x n ↔ x ∈ PiNat.cylinder y n
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>hne : x ≠ y<VAR>i : ℕ<GOAL>x ∈ PiNat.cylinder y i ↔ i ≤ PiNat.firstDiff x y
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<GOAL>x ∈ PiNat.cylinder y (PiNat.firstDiff x y)
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<VAR>hn : n ≤ PiNat.firstDiff x y<GOAL>PiNat.cylinder x n = PiNat.cylinder y n
<VAR>E : ℕ → Type u_1<VAR>x : (n : ℕ) → E n<VAR>n : ℕ<GOAL>⋃ k, PiNat.cylinder (Function.update x n k) (n + 1) = PiNat.cylinder x n
<VAR>E : ℕ → Type u_1<VAR>x : (n : ℕ) → E n<VAR>n : ℕ<VAR>y : E n<GOAL>Function.update x n y ∈ PiNat.cylinder x n
<VAR>α : Type u_2<VAR>x : ℕ → α<GOAL>PiNat.res x 0 = []
<VAR>α : Type u_2<VAR>x : ℕ → α<VAR>n : ℕ<GOAL>PiNat.res x n.succ = x n :: PiNat.res x n
<VAR>α : Type u_2<VAR>x : ℕ → α<VAR>n : ℕ<GOAL>(PiNat.res x n).length = n
<VAR>α : Type u_2<VAR>x y : ℕ → α<VAR>n : ℕ<GOAL>PiNat.res x n = PiNat.res y n ↔ ∀ ⦃m : ℕ⦄, m < n → x m = y m
<VAR>α : Type u_2<GOAL>Function.Injective PiNat.res
<VAR>α : Type u_2<VAR>x : ℕ → α<VAR>n : ℕ<GOAL>PiNat.cylinder x n = {y | PiNat.res y n = PiNat.res x n}
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>h : x ≠ y<GOAL>dist x y = (1 / 2) ^ PiNat.firstDiff x y
<VAR>E : ℕ → Type u_1<VAR>x : (n : ℕ) → E n<GOAL>dist x x = 0
<VAR>E : ℕ → Type u_1<VAR>x y z : (n : ℕ) → E n<GOAL>dist x z ≤ dist x y + dist y z
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<GOAL>y ∈ PiNat.cylinder x n ↔ dist y x ≤ (1 / 2) ^ n
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>f : ((n : ℕ) → E n) → α<GOAL>(∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y) ↔ ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ PiNat.cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<VAR>x : (n : ℕ) → E n<VAR>n : ℕ<GOAL>IsOpen (PiNat.cylinder x n)
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<GOAL>TopologicalSpace.IsTopologicalBasis {s | ∃ x n, s = PiNat.cylinder x n}
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<GOAL>IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<GOAL>CompleteSpace ((n : ℕ) → E n)
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<GOAL>∃ n, Disjoint s (PiNat.cylinder x n)
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x y : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hy : y ∈ s<GOAL>PiNat.firstDiff x y < PiNat.shortestPrefixDiff x s
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<GOAL>0 < PiNat.shortestPrefixDiff x s
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x y : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hy : y ∈ s<GOAL>PiNat.firstDiff x y ≤ PiNat.longestPrefix x s
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>x : (n : ℕ) → E n<GOAL>(s ∩ PiNat.cylinder x (PiNat.longestPrefix x s)).Nonempty
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>n : ℕ<VAR>hn : PiNat.longestPrefix x s < n<GOAL>Disjoint s (PiNat.cylinder x n)
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<VAR>x y : (n : ℕ) → E n<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>H : PiNat.longestPrefix x s < PiNat.firstDiff x y<VAR>xs : x ∉ s<VAR>ys : y ∉ s<GOAL>PiNat.cylinder x (PiNat.longestPrefix x s) = PiNat.cylinder y (PiNat.longestPrefix y s)
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<GOAL>∃ f, (∀ x ∈ s, f x = x) ∧ Set.range f = s ∧ LipschitzWith 1 f
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<GOAL>∃ f, (∀ x ∈ s, f x = x) ∧ Set.range f = s ∧ Continuous f
<VAR>E : ℕ → Type u_1<VAR>(n : ℕ) → TopologicalSpace (E n)<VAR>∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<GOAL>∃ f, (∀ (x : ↑s), f ↑x = x) ∧ Function.Surjective f ∧ Continuous f
<VAR>α : Type u_2<VAR>MetricSpace α<VAR>CompleteSpace α<VAR>SecondCountableTopology α<VAR>Nonempty α<GOAL>∃ f, Continuous f ∧ Function.Surjective f
<VAR>ι : Type u_2<VAR>Encodable ι<VAR>F : ι → Type u_3<VAR>(i : ι) → MetricSpace (F i)<VAR>x y : (i : ι) → F i<GOAL>dist x y = ∑' (i : ι), min ((1 / 2) ^ Encodable.encode i) (dist (x i) (y i))
<VAR>ι : Type u_2<VAR>Encodable ι<VAR>F : ι → Type u_3<VAR>(i : ι) → MetricSpace (F i)<VAR>x y : (i : ι) → F i<GOAL>Summable fun i => min ((1 / 2) ^ Encodable.encode i) (dist (x i) (y i))
<VAR>ι : Type u_2<VAR>Encodable ι<VAR>F : ι → Type u_3<VAR>(i : ι) → MetricSpace (F i)<VAR>x y : (i : ι) → F i<VAR>i : ι<GOAL>min ((1 / 2) ^ Encodable.encode i) (dist (x i) (y i)) ≤ dist x y
<VAR>ι : Type u_2<VAR>Encodable ι<VAR>F : ι → Type u_3<VAR>(i : ι) → MetricSpace (F i)<VAR>x y : (i : ι) → F i<VAR>i : ι<VAR>h : dist x y < (1 / 2) ^ Encodable.encode i<GOAL>dist (x i) (y i) ≤ dist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>self : C(α, β)<GOAL>Continuous self.toFun
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>FunLike F α β<VAR>self : ContinuousMapClass F α β<VAR>f : F<GOAL>Continuous ⇑f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>FunLike F α β<VAR>ContinuousMapClass F α β<VAR>f : F<VAR>a : α<GOAL>ContinuousAt (⇑f) a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>FunLike F α β<VAR>ContinuousMapClass F α β<VAR>f : F<VAR>s : Set α<VAR>a : α<GOAL>ContinuousWithinAt (⇑f) s a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<GOAL>f.toFun = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>F : Type u_5<VAR>FunLike F α β<VAR>ContinuousMapClass F α β<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f g : C(α, β)<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<GOAL>Continuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set C(α, β)<VAR>f : ↑s<GOAL>Continuous ⇑↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<VAR>x : α<GOAL>ContinuousAt (⇑f) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f g : C(α, β)<VAR>H : f = g<VAR>x : α<GOAL>f x = g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<VAR>x y : α<VAR>h : x = y<GOAL>f x = f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<GOAL>Function.Injective DFunLike.coe
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>h : Continuous f<GOAL>⇑{ toFun := f, continuous_toFun := h } = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<VAR>x y : α<VAR>h : x ⤳ y<GOAL>f x ⤳ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>DiscreteTopology α<VAR>f : α → β<GOAL>∀ (a : α), ((ContinuousMap.equivFnOfDiscrete α β).symm f) a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>DiscreteTopology α<VAR>f : C(α, β)<VAR>a : α<GOAL>(ContinuousMap.equivFnOfDiscrete α β) f a = f a
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>⇑(ContinuousMap.id α) = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>b : β<GOAL>⇑(ContinuousMap.const α b) = Function.const α b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace β<GOAL>⇑(ContinuousMap.constPi α) = fun b => Function.const α b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<GOAL>(ContinuousMap.id α) a = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>b : β<VAR>a : α<GOAL>(ContinuousMap.const α b) a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : C(β, γ)<VAR>g : C(α, β)<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : C(β, γ)<VAR>g : C(α, β)<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>f : C(γ, δ)<VAR>g : C(β, γ)<VAR>h : C(α, β)<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<GOAL>(ContinuousMap.id β).comp f = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<GOAL>f.comp (ContinuousMap.id α) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>c : γ<VAR>f : C(α, β)<GOAL>(ContinuousMap.const β c).comp f = ContinuousMap.const α c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : C(β, γ)<VAR>b : β<GOAL>f.comp (ContinuousMap.const α b) = ContinuousMap.const α (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f₁ f₂ : C(β, γ)<VAR>g : C(α, β)<VAR>hg : Function.Surjective ⇑g<GOAL>f₁.comp g = f₂.comp g ↔ f₁ = f₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : C(β, γ)<VAR>g₁ g₂ : C(α, β)<VAR>hf : Function.Injective ⇑f<GOAL>f.comp g₁ = f.comp g₂ ↔ g₁ = g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<GOAL>⇑ContinuousMap.fst = Prod.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<GOAL>⇑ContinuousMap.snd = Prod.snd
<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>TopologicalSpace α₁<VAR>TopologicalSpace α₂<VAR>TopologicalSpace β₁<VAR>TopologicalSpace β₂<VAR>f : C(α₁, α₂)<VAR>g : C(β₁, β₂)<GOAL>∀ (a : α₁ × β₁), (f.prodMap g) a = Prod.map (⇑f) (⇑g) a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>TopologicalSpace β₁<VAR>TopologicalSpace β₂<VAR>f : C(α, β₁)<VAR>g : C(α, β₂)<VAR>a : α<GOAL>(f.prodMk g) a = (f a, g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>x : α × β<GOAL>ContinuousMap.prodSwap x = (x.2, x.1)
<VAR>I : Type u_5<VAR>X : I → Type u_7<VAR>(i : I) → TopologicalSpace (X i)<VAR>i : I<VAR>snd : X i<GOAL>(ContinuousMap.sigmaMk i) snd = ⟨i, snd⟩
<VAR>I : Type u_5<VAR>A : Type u_6<VAR>X : I → Type u_7<VAR>TopologicalSpace A<VAR>(i : I) → TopologicalSpace (X i)<VAR>f : (i : I) → C(X i, A)<VAR>ig : (i : I) × X i<GOAL>(ContinuousMap.sigma f) ig = (f ig.fst) ig.snd
<VAR>I : Type u_5<VAR>A : Type u_6<VAR>X : I → Type u_7<VAR>TopologicalSpace A<VAR>(i : I) → TopologicalSpace (X i)<VAR>f : C((i : I) × X i, A)<VAR>i : I<GOAL>(ContinuousMap.sigmaEquiv A X).symm f i = f.comp (ContinuousMap.sigmaMk i)
<VAR>I : Type u_5<VAR>A : Type u_6<VAR>X : I → Type u_7<VAR>TopologicalSpace A<VAR>(i : I) → TopologicalSpace (X i)<VAR>f : (i : I) → C(X i, A)<GOAL>(ContinuousMap.sigmaEquiv A X) f = ContinuousMap.sigma f
<VAR>I : Type u_5<VAR>A : Type u_6<VAR>X : I → Type u_7<VAR>TopologicalSpace A<VAR>(i : I) → TopologicalSpace (X i)<VAR>f : (i : I) → C(A, X i)<VAR>a : A<GOAL>(ContinuousMap.pi f) a = fun i => (f i) a
<VAR>I : Type u_5<VAR>X : I → Type u_7<VAR>(i : I) → TopologicalSpace (X i)<VAR>i : I<GOAL>⇑(ContinuousMap.eval i) = Function.eval i
<VAR>I : Type u_5<VAR>A : Type u_6<VAR>X : I → Type u_7<VAR>TopologicalSpace A<VAR>(i : I) → TopologicalSpace (X i)<VAR>f : (i : I) → C(A, X i)<GOAL>(ContinuousMap.piEquiv A X) f = ContinuousMap.pi f
<VAR>I : Type u_5<VAR>A : Type u_6<VAR>X : I → Type u_7<VAR>TopologicalSpace A<VAR>(i : I) → TopologicalSpace (X i)<VAR>f : C(A, (i : I) → X i)<VAR>i : I<GOAL>(ContinuousMap.piEquiv A X).symm f i = (ContinuousMap.eval i).comp f
<VAR>I : Type u_5<VAR>X : I → Type u_7<VAR>Y : I → Type u_8<VAR>(i : I) → TopologicalSpace (X i)<VAR>(i : I) → TopologicalSpace (Y i)<VAR>f : (i : I) → C(X i, Y i)<VAR>a : (i : I) → X i<VAR>i : I<GOAL>(ContinuousMap.piMap f) a i = (f i) (a i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set α<VAR>f : C(α, β)<GOAL>⇑(ContinuousMap.restrict s f) = ⇑f ∘ Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<VAR>s : Set α<VAR>x : ↑s<GOAL>(ContinuousMap.restrict s f) x = f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<GOAL>(ContinuousMap.restrict s f) ⟨x, hx⟩ = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>T2Space β<VAR>s : Set α<VAR>hs : Dense s<GOAL>Function.Injective (ContinuousMap.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<VAR>s : Set β<GOAL>∀ (a : ↑(⇑f ⁻¹' s)), (f.restrictPreimage s) a = s.restrictPreimage (⇑f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ι : Type u_5<VAR>S : ι → Set α<VAR>φ : (i : ι) → C(↑(S i), β)<VAR>hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩<VAR>hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x<VAR>i : ι<VAR>x : ↑(S i)<GOAL>(ContinuousMap.liftCover S φ hφ hS) ↑x = (φ i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ι : Type u_5<VAR>S : ι → Set α<VAR>φ : (i : ι) → C(↑(S i), β)<VAR>hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩<VAR>hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x<VAR>i : ι<GOAL>ContinuousMap.restrict (S i) (ContinuousMap.liftCover S φ hφ hS) = φ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>A : Set (Set α)<VAR>F : (s : Set α) → s ∈ A → C(↑s, β)<VAR>hF : ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t), (F s hs) ⟨x, hxi⟩ = (F t ht) ⟨x, hxj⟩<VAR>hA : ∀ (x : α), ∃ i ∈ A, i ∈ 𝓝 x<VAR>s : Set α<VAR>hs : s ∈ A<VAR>x : ↑s<GOAL>(ContinuousMap.liftCover' A F hF hA) ↑x = (F s hs) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>A : Set (Set α)<VAR>F : (s : Set α) → s ∈ A → C(↑s, β)<VAR>hF : ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t), (F s hs) ⟨x, hxi⟩ = (F t ht) ⟨x, hxj⟩<VAR>hA : ∀ (x : α), ∃ i ∈ A, i ∈ 𝓝 x<VAR>s : Set α<VAR>hs : s ∈ A<GOAL>ContinuousMap.restrict s (ContinuousMap.liftCover' A F hF hA) = F s hs
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>f' : C(Y, X)<VAR>hf : Function.RightInverse ⇑f' ⇑f<VAR>b : Y<GOAL>hf.homeomorph.symm b = Quotient.mk'' (f' b)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>f' : C(Y, X)<VAR>hf : Function.RightInverse ⇑f' ⇑f<VAR>a : Quotient (Setoid.ker ⇑f)<GOAL>hf.homeomorph a = a.liftOn' ⇑f ⋯
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<VAR>b : Y<GOAL>hf.homeomorph.symm b = Quotient.mk'' (Function.surjInv ⋯ b)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<VAR>a : Quotient (Setoid.ker ⇑f)<GOAL>hf.homeomorph a = a.liftOn' ⇑f ⋯
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<VAR>g : C(X, Z)<VAR>h : Function.FactorsThrough ⇑g ⇑f<GOAL>∀ (a : Y), (hf.lift g h) a = ((fun i => i.liftOn' ⇑g ⋯) ∘ ⇑hf.homeomorph.symm) a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<VAR>g : C(X, Z)<VAR>h : Function.FactorsThrough ⇑g ⇑f<GOAL>(hf.lift g h).comp f = g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<VAR>g : { g // Function.FactorsThrough ⇑g ⇑f }<GOAL>hf.liftEquiv g = hf.lift ↑g ⋯
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<VAR>g : C(Y, Z)<GOAL>↑(hf.liftEquiv.symm g) = g.comp f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>e : α ≃ₜ β<VAR>a : α<GOAL>e.toContinuousMap a = e a
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>(Homeomorph.refl α).toContinuousMap = ContinuousMap.id α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α ≃ₜ β<VAR>g : β ≃ₜ γ<GOAL>(f.trans g).toContinuousMap = g.toContinuousMap.comp f.toContinuousMap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α ≃ₜ β<GOAL>f.symm.toContinuousMap.comp f.toContinuousMap = ContinuousMap.id α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α ≃ₜ β<GOAL>f.toContinuousMap.comp f.symm.toContinuousMap = ContinuousMap.id β
<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>Y : ι → Type u_3<VAR>TopologicalSpace X<VAR>(i : ι) → TopologicalSpace (Y i)<VAR>Nonempty X<GOAL>Embedding fun g => (ContinuousMap.sigmaMk g.fst).comp g.snd
<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>Y : ι → Type u_3<VAR>TopologicalSpace X<VAR>(i : ι) → TopologicalSpace (Y i)<VAR>ConnectedSpace X<VAR>f : C(X, (i : ι) × Y i)<GOAL>∃ i g, f = (ContinuousMap.sigmaMk i).comp g
<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>Y : ι → Type u_3<VAR>TopologicalSpace X<VAR>(i : ι) → TopologicalSpace (Y i)<VAR>ConnectedSpace X<GOAL>∀ (a : (i : ι) × C(X, Y i)), (ContinuousMap.sigmaCodHomeomorph X Y).symm a = (ContinuousMap.sigmaMk a.fst).comp a.snd
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Monoid Y<VAR>ContinuousMul Y<VAR>f : LocallyConstant X Y<GOAL>LocallyConstant.toContinuousMapMonoidHom f = ↑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>AddMonoid Y<VAR>ContinuousAdd Y<VAR>f : LocallyConstant X Y<GOAL>LocallyConstant.toContinuousMapAddMonoidHom f = ↑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>R : Type u_3<VAR>Semiring R<VAR>AddCommMonoid Y<VAR>Module R Y<VAR>ContinuousAdd Y<VAR>ContinuousConstSMul R Y<VAR>f : LocallyConstant X Y<GOAL>(LocallyConstant.toContinuousMapLinearMap R) f = ↑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>R : Type u_3<VAR>CommSemiring R<VAR>Semiring Y<VAR>Algebra R Y<VAR>TopologicalSemiring Y<VAR>f : LocallyConstant X Y<GOAL>(LocallyConstant.toContinuousMapAlgHom R) f = ↑f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>x : α<VAR>s t : Set α<VAR>h : LowerSemicontinuousWithinAt f s x<VAR>hst : t ⊆ s<GOAL>LowerSemicontinuousWithinAt f t x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>x : α<GOAL>LowerSemicontinuousWithinAt f Set.univ x ↔ LowerSemicontinuousAt f x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>x : α<VAR>s : Set α<VAR>h : LowerSemicontinuousAt f x<GOAL>LowerSemicontinuousWithinAt f s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>x : α<VAR>s : Set α<VAR>h : LowerSemicontinuousOn f s<VAR>hx : x ∈ s<GOAL>LowerSemicontinuousWithinAt f s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>h : LowerSemicontinuousOn f s<VAR>hst : t ⊆ s<GOAL>LowerSemicontinuousOn f t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<GOAL>LowerSemicontinuousOn f Set.univ ↔ LowerSemicontinuous f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>h : LowerSemicontinuous f<VAR>x : α<GOAL>LowerSemicontinuousAt f x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>h : LowerSemicontinuous f<VAR>s : Set α<VAR>x : α<GOAL>LowerSemicontinuousWithinAt f s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>f : α → β<VAR>h : LowerSemicontinuous f<VAR>s : Set α<GOAL>LowerSemicontinuousOn f s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>x : α<VAR>s : Set α<VAR>z : β<GOAL>LowerSemicontinuousWithinAt (fun _x => z) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>x : α<VAR>z : β<GOAL>LowerSemicontinuousAt (fun _x => z) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>s : Set α<VAR>z : β<GOAL>LowerSemicontinuousOn (fun _x => z) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>z : β<GOAL>LowerSemicontinuous fun _x => z
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>s : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsOpen s<VAR>hy : 0 ≤ y<GOAL>LowerSemicontinuous (s.indicator fun _x => y)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>s t : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsOpen s<VAR>hy : 0 ≤ y<GOAL>LowerSemicontinuousOn (s.indicator fun _x => y) t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>x : α<VAR>s : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsOpen s<VAR>hy : 0 ≤ y<GOAL>LowerSemicontinuousAt (s.indicator fun _x => y) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>x : α<VAR>s t : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsOpen s<VAR>hy : 0 ≤ y<GOAL>LowerSemicontinuousWithinAt (s.indicator fun _x => y) t x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>s : Set α<VAR>y : β<VAR>Zero β<VAR>hs : IsClosed s<VAR>hy : y ≤ 0<GOAL>LowerSemicontinuous (s.indicator fun _x => y)