ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>self : f₀.Homotopy f₁<VAR>x : X<GOAL>self.toFun (0, x) = f₀ x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>self : f₀.Homotopy f₁<VAR>x : X<GOAL>self.toFun (1, x) = f₁ x
<VAR>X : outParam (Type u_3)<VAR>Y : outParam (Type u_4)<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>F : Type u_5<VAR>f₀ f₁ : outParam C(X, Y)<VAR>FunLike F (↑I × X) Y<VAR>self : ContinuousMap.HomotopyLike F f₀ f₁<VAR>f : F<VAR>x : X<GOAL>f (0, x) = f₀ x
<VAR>X : outParam (Type u_3)<VAR>Y : outParam (Type u_4)<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>F : Type u_5<VAR>f₀ f₁ : outParam C(X, Y)<VAR>FunLike F (↑I × X) Y<VAR>self : ContinuousMap.HomotopyLike F f₀ f₁<VAR>f : F<VAR>x : X<GOAL>f (1, x) = f₁ x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F G : f₀.Homotopy f₁<VAR>h : ∀ (x : ↑I × X), F x = G x<GOAL>F = G
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<GOAL>Continuous ⇑F
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>x : X<GOAL>F (0, x) = f₀ x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>x : X<GOAL>F (1, x) = f₁ x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<GOAL>⇑F.toContinuousMap = ⇑F
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>t : ↑I<VAR>x : X<GOAL>(F.curry t) x = F (t, x)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>t : ℝ<VAR>ht : t ≤ 0<VAR>x : X<GOAL>(F.extend t) x = f₀ x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>t : ℝ<VAR>ht : 1 ≤ t<VAR>x : X<GOAL>(F.extend t) x = f₁ x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>t : ↑I<VAR>x : X<GOAL>(F.extend ↑t) x = F (t, x)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>t : ℝ<VAR>ht : t ∈ I<VAR>x : X<GOAL>(F.extend t) x = F (⟨t, ht⟩, x)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F G : f₀.Homotopy f₁<VAR>h : F = G<VAR>x : ↑I × X<GOAL>F x = G x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>x y : ↑I × X<VAR>h : x = y<GOAL>F x = F y
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>x : ↑I × X<GOAL>(ContinuousMap.Homotopy.refl f) x = f x.2
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>x : ↑I × X<GOAL>F.symm x = F (σ x.1, x.2)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<GOAL>F.symm.symm = F
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<GOAL>Function.Bijective ContinuousMap.Homotopy.symm
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ f₂ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>G : f₁.Homotopy f₂<VAR>x : ↑I × X<GOAL>(F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ f₂ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>G : f₁.Homotopy f₂<GOAL>(F.trans G).symm = G.symm.trans F.symm
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ g₀ g₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>h₀ : f₀ = g₀<VAR>h₁ : f₁ = g₁<VAR>a : ↑I × X<GOAL>(F.cast h₀ h₁) a = F a
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>g₀ g₁ : C(Y, Z)<VAR>G : g₀.Homotopy g₁<VAR>f : C(X, Y)<GOAL>∀ (a : ↑I × X), (G.compContinuousMap f) a = G (Prod.map id (⇑f) a)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f₀ f₁ : C(X, Y)<VAR>g₀ g₁ : C(Y, Z)<VAR>F : f₀.Homotopy f₁<VAR>G : g₀.Homotopy g₁<VAR>x : ↑I × X<GOAL>(F.hcomp G) x = G (x.1, F x)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<GOAL>f.Homotopic f
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f g : C(X, Y)<VAR>h : f.Homotopic g<GOAL>g.Homotopic f
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f g h : C(X, Y)<VAR>h₀ : f.Homotopic g<VAR>h₁ : g.Homotopic h<GOAL>f.Homotopic h
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f₀ f₁ : C(X, Y)<VAR>g₀ g₁ : C(Y, Z)<VAR>h₀ : f₀.Homotopic f₁<VAR>h₁ : g₀.Homotopic g₁<GOAL>(g₀.comp f₀).Homotopic (g₁.comp f₁)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Equivalence ContinuousMap.Homotopic
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f₀ f₁ : C(X, Y)<VAR>g₀ g₁ : C(X, Z)<GOAL>f₀.Homotopic f₁ → g₀.Homotopic g₁ → (f₀.prodMk g₀).Homotopic (f₁.prodMk g₁)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace Z'<VAR>f₀ f₁ : C(X, Y)<VAR>g₀ g₁ : C(Z, Z')<GOAL>f₀.Homotopic f₁ → g₀.Homotopic g₁ → (f₀.prodMap g₀).Homotopic (f₁.prodMap g₁)
<VAR>X : Type u<VAR>ι : Type u_2<VAR>TopologicalSpace X<VAR>Y : ι → Type u_3<VAR>(i : ι) → TopologicalSpace (Y i)<VAR>f₀ f₁ : (i : ι) → C(X, Y i)<VAR>F : ∀ (i : ι), (f₀ i).Homotopic (f₁ i)<GOAL>(ContinuousMap.pi f₀).Homotopic (ContinuousMap.pi f₁)
<VAR>ι : Type u_2<VAR>X : ι → Type u_3<VAR>Y : ι → Type u_4<VAR>(i : ι) → TopologicalSpace (X i)<VAR>(i : ι) → TopologicalSpace (Y i)<VAR>f₀ f₁ : (i : ι) → C(X i, Y i)<VAR>F : ∀ (i : ι), (f₀ i).Homotopic (f₁ i)<GOAL>(ContinuousMap.piMap f₀).Homotopic (ContinuousMap.piMap f₁)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>P : C(X, Y) → Prop<VAR>self : f₀.HomotopyWith f₁ P<VAR>t : ↑I<GOAL>P { toFun := fun x => self.toFun (t, x), continuous_toFun := ⋯ }
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>P : C(X, Y) → Prop<GOAL>Function.Injective DFunLike.coe
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>P : C(X, Y) → Prop<VAR>F G : f₀.HomotopyWith f₁ P<VAR>h : ∀ (x : ↑I × X), F x = G x<GOAL>F = G
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>P : C(X, Y) → Prop<VAR>F : f₀.HomotopyWith f₁ P<GOAL>Continuous ⇑F
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>P : C(X, Y) → Prop<VAR>F : f₀.HomotopyWith f₁ P<VAR>x : X<GOAL>F (0, x) = f₀ x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>P : C(X, Y) → Prop<VAR>F : f₀.HomotopyWith f₁ P<VAR>x : X<GOAL>F (1, x) = f₁ x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>P : C(X, Y) → Prop<VAR>F : f₀.HomotopyWith f₁ P<GOAL>⇑F.toContinuousMap = ⇑F
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>P : C(X, Y) → Prop<VAR>F : f₀.HomotopyWith f₁ P<GOAL>⇑F.toHomotopy = ⇑F
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>P : C(X, Y) → Prop<VAR>F : f₀.HomotopyWith f₁ P<VAR>t : ↑I<GOAL>P (F.curry t)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>P : C(X, Y) → Prop<VAR>F : f₀.HomotopyWith f₁ P<VAR>t : ℝ<GOAL>P (F.extend t)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>P : C(X, Y) → Prop<VAR>f : C(X, Y)<VAR>hf : P f<VAR>x : ↑I × X<GOAL>(ContinuousMap.HomotopyWith.refl f hf) x = f x.2
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>P : C(X, Y) → Prop<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.HomotopyWith f₁ P<VAR>x : ↑I × X<GOAL>F.symm x = F (σ x.1, x.2)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>P : C(X, Y) → Prop<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.HomotopyWith f₁ P<GOAL>F.symm.symm = F
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>P : C(X, Y) → Prop<VAR>f₀ f₁ : C(X, Y)<GOAL>Function.Bijective ContinuousMap.HomotopyWith.symm
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>P : C(X, Y) → Prop<VAR>f₀ f₁ f₂ : C(X, Y)<VAR>F : f₀.HomotopyWith f₁ P<VAR>G : f₁.HomotopyWith f₂ P<VAR>x : ↑I × X<GOAL>(F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>P : C(X, Y) → Prop<VAR>f₀ f₁ f₂ : C(X, Y)<VAR>F : f₀.HomotopyWith f₁ P<VAR>G : f₁.HomotopyWith f₂ P<GOAL>(F.trans G).symm = G.symm.trans F.symm
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>P : C(X, Y) → Prop<VAR>f₀ f₁ g₀ g₁ : C(X, Y)<VAR>F : f₀.HomotopyWith f₁ P<VAR>h₀ : f₀ = g₀<VAR>h₁ : f₁ = g₁<VAR>a : ↑I × X<GOAL>(F.cast h₀ h₁) a = F a
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>P : C(X, Y) → Prop<VAR>f : C(X, Y)<VAR>hf : P f<GOAL>f.HomotopicWith f P
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>P : C(X, Y) → Prop<VAR>f g : C(X, Y)<VAR>h : f.HomotopicWith g P<GOAL>g.HomotopicWith f P
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>P : C(X, Y) → Prop<VAR>f g h : C(X, Y)<VAR>h₀ : f.HomotopicWith g P<VAR>h₁ : g.HomotopicWith h P<GOAL>f.HomotopicWith h P
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>S : Set X<VAR>F : f₀.HomotopyRel f₁ S<VAR>t : ↑I<VAR>x : X<VAR>hx : x ∈ S<GOAL>F (t, x) = f₀ x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>S : Set X<VAR>F : f₀.HomotopyRel f₁ S<VAR>t : ↑I<VAR>x : X<VAR>hx : x ∈ S<GOAL>F (t, x) = f₁ x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>S : Set X<VAR>F : f₀.HomotopyRel f₁ S<VAR>x : X<VAR>hx : x ∈ S<GOAL>f₀ x = f₁ x
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>S : Set X<VAR>x : ↑I × X<GOAL>(ContinuousMap.HomotopyRel.refl f S) x = f x.2
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>S : Set X<VAR>F : f₀.HomotopyRel f₁ S<VAR>x : ↑I × X<GOAL>F.symm x = F (σ x.1, x.2)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>S : Set X<VAR>F : f₀.HomotopyRel f₁ S<GOAL>F.symm.symm = F
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<VAR>S : Set X<GOAL>Function.Bijective ContinuousMap.HomotopyRel.symm
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ f₂ : C(X, Y)<VAR>S : Set X<VAR>F : f₀.HomotopyRel f₁ S<VAR>G : f₁.HomotopyRel f₂ S<VAR>x : ↑I × X<GOAL>(F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ f₂ : C(X, Y)<VAR>S : Set X<VAR>F : f₀.HomotopyRel f₁ S<VAR>G : f₁.HomotopyRel f₂ S<GOAL>(F.trans G).symm = G.symm.trans F.symm
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>S : Set X<VAR>f₀ f₁ g₀ g₁ : C(X, Y)<VAR>F : f₀.HomotopyRel f₁ S<VAR>h₀ : f₀ = g₀<VAR>h₁ : f₁ = g₁<VAR>a : ↑I × X<GOAL>(F.cast h₀ h₁) a = F a
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>S : Set X<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.HomotopyRel f₁ S<VAR>g : C(Y, Z)<VAR>x : ↑I × X<GOAL>(F.compContinuousMap g) x = g (F x)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>S : Set X<VAR>f₀ f₁ : C(X, Y)<VAR>h : f₀.HomotopicRel f₁ S<GOAL>f₀.Homotopic f₁
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>S : Set X<VAR>f : C(X, Y)<GOAL>f.HomotopicRel f S
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>S : Set X<VAR>f g : C(X, Y)<VAR>h : f.HomotopicRel g S<GOAL>g.HomotopicRel f S
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>S : Set X<VAR>f g h : C(X, Y)<VAR>h₀ : f.HomotopicRel g S<VAR>h₁ : g.HomotopicRel h S<GOAL>f.HomotopicRel h S
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>S : Set X<GOAL>Equivalence fun f g => f.HomotopicRel g S
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f₀ f₁ : C(X, Y)<GOAL>f₀.HomotopicRel f₁ ∅ ↔ f₀.Homotopic f₁
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>Filter.Tendsto f Filter.cofinite (Filter.cocompact Y) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>T1Space X<VAR>WeaklyLocallyCompactSpace Y<VAR>hf' : Continuous f<VAR>hf : Filter.Tendsto f Filter.cofinite (Filter.cocompact Y)<GOAL>DiscreteTopology X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>DiscreteTopology X<VAR>hf : Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)<GOAL>Filter.Tendsto f Filter.cofinite (Filter.cocompact Y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>_hs' : DiscreteTopology ↑s<GOAL>Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact X)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>WeaklyLocallyCompactSpace X<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact X) ↔ DiscreteTopology ↑s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set X<GOAL>IsClosed S ∧ DiscreteTopology ↑S ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<GOAL>∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>a b : ℝ<VAR>hle : a ≤ b<GOAL>∃ f, Set.EqOn (⇑f) (Function.const X a) s ∧ Set.EqOn (⇑f) (Function.const X b) t ∧ ∀ (x : X), f x ∈ Set.Icc a b
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<GOAL>IsSigmaCompact s
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>IsSigmaCompact ∅
<VAR>X : Type u_1<VAR>ι : Type u_3<VAR>TopologicalSpace X<VAR>hι : Countable ι<VAR>s : ι → Set X<VAR>hcomp : ∀ (i : ι), IsCompact (s i)<GOAL>IsSigmaCompact (⋃ i, s i)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>hc : S.Countable<VAR>hcomp : ∀ s ∈ S, IsCompact s<GOAL>IsSigmaCompact (⋃₀ S)
<VAR>X : Type u_1<VAR>ι : Type u_3<VAR>TopologicalSpace X<VAR>Countable ι<VAR>s : ι → Set X<VAR>hcomp : ∀ (i : ι), IsSigmaCompact (s i)<GOAL>IsSigmaCompact (⋃ i, s i)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>hc : S.Countable<VAR>hcomp : ∀ (s : ↑S), IsSigmaCompact ↑s<GOAL>IsSigmaCompact (⋃₀ S)
<VAR>X : Type u_1<VAR>ι : Type u_3<VAR>TopologicalSpace X<VAR>s : Set ι<VAR>S : ι → Set X<VAR>hc : s.Countable<VAR>hcomp : ∀ i ∈ s, IsSigmaCompact (S i)<GOAL>IsSigmaCompact (⋃ i ∈ s, S i)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>ht : IsSigmaCompact t<VAR>hs : IsClosed s<VAR>h : s ⊆ t<GOAL>IsSigmaCompact s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>hs : IsSigmaCompact s<VAR>hf : ContinuousOn f s<GOAL>IsSigmaCompact (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>s : Set X<VAR>hs : IsSigmaCompact s<GOAL>IsSigmaCompact (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>hf : Inducing f<GOAL>IsSigmaCompact s ↔ IsSigmaCompact (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>hf : Embedding f<GOAL>IsSigmaCompact s ↔ IsSigmaCompact (f '' s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>p : X → Prop<VAR>s : Set { a // p a }<GOAL>IsSigmaCompact s ↔ IsSigmaCompact (Subtype.val '' s)
<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>self : SigmaCompactSpace X<GOAL>IsSigmaCompact Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>IsSigmaCompact Set.univ ↔ SigmaCompactSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>h : SigmaCompactSpace X<GOAL>IsSigmaCompact Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>SigmaCompactSpace X ↔ ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>h : SigmaCompactSpace X<GOAL>∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = Set.univ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>SigmaCompactSpace X<GOAL>IsSigmaCompact (Set.range f)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsSigmaCompact s ↔ IsSigmaCompact Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsSigmaCompact s ↔ SigmaCompactSpace ↑s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>Hc : S.Countable<VAR>Hcomp : ∀ s ∈ S, IsCompact s<VAR>HU : ⋃₀ S = Set.univ<GOAL>SigmaCompactSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>SigmaCompactSpace X<VAR>n : ℕ<GOAL>IsCompact (compactCovering X n)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>SigmaCompactSpace X<GOAL>⋃ n, compactCovering X n = Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>SigmaCompactSpace X<GOAL>⋃ n, closure (compactCovering X n) = Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>SigmaCompactSpace X<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>compactCovering X m ⊆ compactCovering X n
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>SigmaCompactSpace X<VAR>x : X<GOAL>∃ n, x ∈ compactCovering X n
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>SigmaCompactSpace X<VAR>e : Y → X<VAR>he : ClosedEmbedding e<GOAL>SigmaCompactSpace Y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>SigmaCompactSpace X<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>SigmaCompactSpace ↑s
<VAR>X : Type u_1<VAR>ι : Type u_3<VAR>TopologicalSpace X<VAR>SigmaCompactSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>hne : ∀ (i : ι), (f i).Nonempty<GOAL>Set.univ.Countable
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>SigmaCompactSpace X<VAR>f : X → Set X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hf : ∀ x ∈ s, f x ∈ 𝓝[s] x<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>SigmaCompactSpace X<VAR>f : X → Set X<VAR>hf : ∀ (x : X), f x ∈ 𝓝 x<GOAL>∃ s, s.Countable ∧ ⋃ x ∈ s, f x = Set.univ
<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>self : CompactExhaustion X<VAR>n : ℕ<GOAL>self.toFun n ⊆ interior (self.toFun (n + 1))
<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>self : CompactExhaustion X<GOAL>⋃ n, self.toFun n = Set.univ
<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>self : CompactExhaustion X<VAR>n : ℕ<GOAL>IsCompact (self.toFun n)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>K : CompactExhaustion X<GOAL>K.toFun = ⇑K
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>K : CompactExhaustion X<VAR>n : ℕ<GOAL>IsCompact (K n)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>K : CompactExhaustion X<VAR>n : ℕ<GOAL>K n ⊆ interior (K (n + 1))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>K : CompactExhaustion X<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>K m ⊆ K n
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>K : CompactExhaustion X<VAR>n : ℕ<GOAL>K n ⊆ K (n + 1)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>K : CompactExhaustion X<VAR>m n : ℕ<VAR>h : m < n<GOAL>K m ⊆ interior (K n)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>K : CompactExhaustion X<GOAL>⋃ n, K n = Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>K : CompactExhaustion X<VAR>x : X<GOAL>∃ n, x ∈ K n
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>K : CompactExhaustion X<VAR>s : Set X<VAR>hs : IsCompact s<GOAL>∃ n, s ⊆ K n
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>K : CompactExhaustion X<VAR>x : X<GOAL>x ∈ K (K.find x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>K : CompactExhaustion X<VAR>x : X<VAR>n : ℕ<GOAL>x ∈ K n ↔ K.find x ≤ n
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>K : CompactExhaustion X<VAR>x : X<GOAL>K.shiftr.find x = K.find x + 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>K : CompactExhaustion X<VAR>x : X<GOAL>x ∈ K.shiftr (K.find x + 1) \ K.shiftr (K.find x)
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>self : DiscreteQuotient X<VAR>x : X<GOAL>IsOpen (setOf (self.Rel x))
<VAR>X : Type u_2<VAR>TopologicalSpace X<GOAL>Function.Injective DiscreteQuotient.toSetoid
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>S : DiscreteQuotient X<VAR>x : X<GOAL>S.Rel x x
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>S : DiscreteQuotient X<VAR>x y : X<GOAL>S.Rel x y → S.Rel y x
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>S : DiscreteQuotient X<VAR>x y z : X<GOAL>S.Rel x y → S.Rel y z → S.Rel x z
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>S : DiscreteQuotient X<VAR>x : X<GOAL>S.proj ⁻¹' {S.proj x} = setOf (S.Rel x)
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>S : DiscreteQuotient X<GOAL>Function.Surjective S.proj
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>S : DiscreteQuotient X<GOAL>QuotientMap S.proj
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>S : DiscreteQuotient X<GOAL>Continuous S.proj
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>S : DiscreteQuotient X<GOAL>IsLocallyConstant S.proj
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>S : DiscreteQuotient X<VAR>A : Set (Quotient S.toSetoid)<GOAL>IsClopen (S.proj ⁻¹' A)
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>S : DiscreteQuotient X<VAR>A : Set (Quotient S.toSetoid)<GOAL>IsOpen (S.proj ⁻¹' A)
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>S : DiscreteQuotient X<VAR>A : Set (Quotient S.toSetoid)<GOAL>IsClosed (S.proj ⁻¹' A)
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>S : DiscreteQuotient X<VAR>x : X<GOAL>IsClopen (setOf (S.Rel x))
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>S : DiscreteQuotient X<GOAL>DiscreteQuotient.comap (ContinuousMap.id X) S = S
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>g : C(Y, Z)<VAR>f : C(X, Y)<VAR>S : DiscreteQuotient Z<GOAL>DiscreteQuotient.comap (g.comp f) S = DiscreteQuotient.comap f (DiscreteQuotient.comap g S)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>A B : DiscreteQuotient Y<VAR>h : A ≤ B<GOAL>DiscreteQuotient.comap f A ≤ DiscreteQuotient.comap f B
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>A : DiscreteQuotient X<GOAL>DiscreteQuotient.ofLE ⋯ = id
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>A : DiscreteQuotient X<VAR>a : Quotient A.toSetoid<GOAL>DiscreteQuotient.ofLE ⋯ a = a
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>A B C : DiscreteQuotient X<VAR>h₁ : A ≤ B<VAR>h₂ : B ≤ C<VAR>x : Quotient A.toSetoid<GOAL>DiscreteQuotient.ofLE h₂ (DiscreteQuotient.ofLE h₁ x) = DiscreteQuotient.ofLE ⋯ x
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>A B C : DiscreteQuotient X<VAR>h₁ : A ≤ B<VAR>h₂ : B ≤ C<GOAL>DiscreteQuotient.ofLE h₂ ∘ DiscreteQuotient.ofLE h₁ = DiscreteQuotient.ofLE ⋯
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>A B : DiscreteQuotient X<VAR>h : A ≤ B<GOAL>Continuous (DiscreteQuotient.ofLE h)
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>A B : DiscreteQuotient X<VAR>h : A ≤ B<VAR>x : X<GOAL>DiscreteQuotient.ofLE h (A.proj x) = B.proj x