ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>ι : Sort u_3<VAR>t : ι → TopologicalSpace X<VAR>h : ∀ (i : ι), SequentialSpace X<GOAL>SequentialSpace X
<VAR>X : Type u_1<VAR>t₁ t₂ : TopologicalSpace X<VAR>h₁ : SequentialSpace X<VAR>h₂ : SequentialSpace X<GOAL>SequentialSpace X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>SequentialSpace X<VAR>f : X → Y<VAR>hf : QuotientMap f<GOAL>SequentialSpace Y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsSeqCompact s<VAR>x : ℕ → X<VAR>hx : ∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s<GOAL>∃ a ∈ s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (𝓝 a)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>SeqCompactSpace X<VAR>x : ℕ → X<GOAL>∃ a φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (𝓝 a)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>s : Set X<VAR>hs : IsCompact s<GOAL>IsSeqCompact s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>s : Set X<VAR>x : ℕ → X<VAR>hs : IsCompact s<VAR>hx : ∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s<GOAL>∃ a ∈ s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (𝓝 a)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>s : Set X<VAR>x : ℕ → X<VAR>hs : IsCompact s<VAR>hx : ∀ (n : ℕ), x n ∈ s<GOAL>∃ a ∈ s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (𝓝 a)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>CompactSpace X<VAR>x : ℕ → X<GOAL>∃ a φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (𝓝 a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>f_cont : SeqContinuous f<VAR>K : Set X<VAR>K_cpt : IsSeqCompact K<GOAL>IsSeqCompact (f '' K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>SeqCompactSpace X<VAR>f_cont : SeqContinuous f<GOAL>IsSeqCompact (Set.range f)
<VAR>X : Type u_1<VAR>UniformSpace X<VAR>s : Set X<VAR>hs : IsSeqCompact s<VAR>u : ℕ → X<VAR>hu : ∃ᶠ (n : ℕ) in Filter.atTop, u n ∈ s<VAR>huc : CauchySeq u<GOAL>∃ x ∈ s, Filter.Tendsto u Filter.atTop (𝓝 x)
<VAR>X : Type u_1<VAR>UniformSpace X<VAR>s : Set X<VAR>hs : IsSeqCompact s<VAR>u : ℕ → X<VAR>hu : ∀ (n : ℕ), u n ∈ s<VAR>huc : CauchySeq u<GOAL>∃ x ∈ s, Filter.Tendsto u Filter.atTop (𝓝 x)
<VAR>X : Type u_1<VAR>UniformSpace X<VAR>s : Set X<VAR>h : IsSeqCompact s<GOAL>TotallyBounded s
<VAR>X : Type u_1<VAR>UniformSpace X<VAR>s : Set X<VAR>(𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<GOAL>IsComplete s
<VAR>X : Type u_1<VAR>UniformSpace X<VAR>s : Set X<VAR>(𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<GOAL>IsCompact s
<VAR>X : Type u_1<VAR>UniformSpace X<VAR>s : Set X<VAR>(𝓤 X).IsCountablyGenerated<GOAL>IsCompact s ↔ IsSeqCompact s
<VAR>X : Type u_1<VAR>UniformSpace X<VAR>(𝓤 X).IsCountablyGenerated<GOAL>CompactSpace X ↔ SeqCompactSpace X
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a b : α<VAR>hab : a < b<VAR>s : Set α<GOAL>[s ∈ 𝓝[>] a, s ∈ 𝓝[Set.Ioc a b] a, s ∈ 𝓝[Set.Ioo a b] a, ∃ u ∈ Set.Ioc a b, Set.Ioo a u ⊆ s, ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s].TFAE
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a u' : α<VAR>s : Set α<VAR>hu' : a < u'<GOAL>s ∈ 𝓝[>] a ↔ ∃ u ∈ Set.Ioc a u', Set.Ioo a u ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a u' : α<VAR>s : Set α<VAR>hu' : a < u'<GOAL>s ∈ 𝓝[>] a ↔ ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>h : ∃ b, a < b<GOAL>(𝓝[>] a).HasBasis (fun x => a < x) (Set.Ioo a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>a : α<GOAL>(𝓝[>] a).HasBasis (fun x => a < x) (Set.Ioo a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<GOAL>𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ 𝓝[>] a ↔ ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<GOAL>{x | 𝓝[>] x = ⊥}.Countable
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<GOAL>{x | 𝓝[<] x = ⊥}.Countable
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>DenselyOrdered α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ 𝓝[>] a ↔ ∃ u ∈ Set.Ioi a, Set.Ioc a u ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a b : α<VAR>h : a < b<VAR>s : Set α<GOAL>[s ∈ 𝓝[<] b, s ∈ 𝓝[Set.Ico a b] b, s ∈ 𝓝[Set.Ioo a b] b, ∃ l ∈ Set.Ico a b, Set.Ioo l b ⊆ s, ∃ l ∈ Set.Iio b, Set.Ioo l b ⊆ s].TFAE
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a l' : α<VAR>s : Set α<VAR>hl' : l' < a<GOAL>s ∈ 𝓝[<] a ↔ ∃ l ∈ Set.Ico l' a, Set.Ioo l a ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a l' : α<VAR>s : Set α<VAR>hl' : l' < a<GOAL>s ∈ 𝓝[<] a ↔ ∃ l ∈ Set.Iio a, Set.Ioo l a ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMinOrder α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ 𝓝[<] a ↔ ∃ l ∈ Set.Iio a, Set.Ioo l a ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMinOrder α<VAR>DenselyOrdered α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ 𝓝[<] a ↔ ∃ l ∈ Set.Iio a, Set.Ico l a ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>h : ∃ b, b < a<GOAL>(𝓝[<] a).HasBasis (fun x => x < a) fun x => Set.Ioo x a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<GOAL>𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a b : α<VAR>hab : a < b<VAR>s : Set α<GOAL>[s ∈ 𝓝[≥] a, s ∈ 𝓝[Set.Icc a b] a, s ∈ 𝓝[Set.Ico a b] a, ∃ u ∈ Set.Ioc a b, Set.Ico a u ⊆ s, ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s].TFAE
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a u' : α<VAR>s : Set α<VAR>hu' : a < u'<GOAL>s ∈ 𝓝[≥] a ↔ ∃ u ∈ Set.Ioc a u', Set.Ico a u ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a u' : α<VAR>s : Set α<VAR>hu' : a < u'<GOAL>s ∈ 𝓝[≥] a ↔ ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ 𝓝[≥] a ↔ ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>a : α<GOAL>(𝓝[≥] a).HasBasis (fun u => a < u) (Set.Ico a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>DenselyOrdered α<VAR>a : α<GOAL>(𝓝[≥] a).HasBasis (fun x => a < x) (Set.Icc a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>DenselyOrdered α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ 𝓝[≥] a ↔ ∃ u, a < u ∧ Set.Icc a u ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a b : α<VAR>h : a < b<VAR>s : Set α<GOAL>[s ∈ 𝓝[≤] b, s ∈ 𝓝[Set.Icc a b] b, s ∈ 𝓝[Set.Ioc a b] b, ∃ l ∈ Set.Ico a b, Set.Ioc l b ⊆ s, ∃ l ∈ Set.Iio b, Set.Ioc l b ⊆ s].TFAE
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a l' : α<VAR>s : Set α<VAR>hl' : l' < a<GOAL>s ∈ 𝓝[≤] a ↔ ∃ l ∈ Set.Ico l' a, Set.Ioc l a ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a l' : α<VAR>s : Set α<VAR>hl' : l' < a<GOAL>s ∈ 𝓝[≤] a ↔ ∃ l ∈ Set.Iio a, Set.Ioc l a ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMinOrder α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ 𝓝[≤] a ↔ ∃ l ∈ Set.Iio a, Set.Ioc l a ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMinOrder α<VAR>DenselyOrdered α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ 𝓝[≤] a ↔ ∃ l < a, Set.Icc l a ⊆ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMinOrder α<VAR>DenselyOrdered α<VAR>a : α<GOAL>(𝓝[≤] a).HasBasis (fun x => x < a) fun x => Set.Icc x a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrderedAddCommGroup α<VAR>OrderTopology α<VAR>a : α<GOAL>𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}
<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>LinearOrderedAddCommGroup α<VAR>h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}<GOAL>OrderTopology α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrderedAddCommGroup α<VAR>OrderTopology α<VAR>f : β → α<VAR>x : Filter β<VAR>a : α<GOAL>Filter.Tendsto f x (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ (b : β) in x, |f b - a| < ε
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrderedAddCommGroup α<VAR>OrderTopology α<VAR>a : α<VAR>ε : α<VAR>hε : 0 < ε<GOAL>∀ᶠ (x : α) in 𝓝 a, |x - a| < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrderedAddCommGroup α<VAR>OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>C : α<VAR>hf : Filter.Tendsto f l (𝓝 C)<VAR>hg : Filter.Tendsto g l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrderedAddCommGroup α<VAR>OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>C : α<VAR>hf : Filter.Tendsto f l (𝓝 C)<VAR>hg : Filter.Tendsto g l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrderedAddCommGroup α<VAR>OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>C : α<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>hg : Filter.Tendsto g l (𝓝 C)<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrderedAddCommGroup α<VAR>OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>C : α<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>hg : Filter.Tendsto g l (𝓝 C)<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrderedAddCommGroup α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>a : α<GOAL>(𝓝 a).HasBasis (fun ε => 0 < ε) fun ε => {b | |b - a| < ε}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrderedAddCommGroup α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>a : α<GOAL>(𝓝 a).HasBasis (fun ε => 0 < ε) fun ε => Set.Ioo (a - ε) (a + ε)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrderedAddCommGroup α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>DenselyOrdered α<VAR>a : α<GOAL>(𝓝 a).HasBasis (fun x => 0 < x) fun ε => Set.Icc (a - ε) (a + ε)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrderedAddCommGroup α<VAR>OrderTopology α<VAR>NoMaxOrder α<GOAL>(𝓝 0).HasBasis (fun ε => 0 < ε) fun ε => {b | |b| < ε}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrderedAddCommGroup α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>a : α<VAR>ha : 0 < a<GOAL>(𝓝 a).HasBasis (fun ε => 0 < ε ∧ ε ≤ a) fun ε => Set.Ioo (a - ε) (a + ε)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMaxOrder α<VAR>S : Set α<VAR>hS : S.OrdConnected<VAR>x y : α<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<GOAL>S ∈ 𝓝[≥] x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMaxOrder α<VAR>S : Set α<VAR>hS : S.OrdConnected<VAR>x y : α<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<GOAL>S ∈ 𝓝[>] x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>S : Set α<VAR>hS : S.OrdConnected<VAR>x y : α<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<GOAL>S ∈ 𝓝[≤] y
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>S : Set α<VAR>hS : S.OrdConnected<VAR>x y : α<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<GOAL>S ∈ 𝓝[<] y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>y : Y<GOAL>(ContinuousMap.const X y).Nullhomotopic
<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 : f.Nullhomotopic<VAR>g : C(Y, Z)<GOAL>(g.comp f).Nullhomotopic
<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(Y, Z)<VAR>hf : f.Nullhomotopic<VAR>g : C(X, Y)<GOAL>(f.comp g).Nullhomotopic
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>self : ContractibleSpace X<GOAL>Nonempty (X ≃ₕ Unit)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ContractibleSpace X<GOAL>Nonempty (X ≃ₕ Unit)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ContractibleSpace X<GOAL>(ContinuousMap.id X).Nullhomotopic
<VAR>Y : Type u_1<VAR>TopologicalSpace Y<GOAL>ContractibleSpace Y ↔ (ContinuousMap.id Y).Nullhomotopic
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>ContractibleSpace Y<VAR>e : X ≃ₕ Y<GOAL>ContractibleSpace X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₕ Y<GOAL>ContractibleSpace X ↔ ContractibleSpace Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>ContractibleSpace Y<VAR>e : X ≃ₜ Y<GOAL>ContractibleSpace X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<GOAL>ContractibleSpace X ↔ ContractibleSpace Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>ContractibleSpace X<VAR>ContractibleSpace Y<GOAL>Nonempty (X ≃ₕ Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>self : X ≃ₕ Y<GOAL>(self.toFun.comp self.invFun).Homotopic (ContinuousMap.id Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>self : X ≃ₕ Y<GOAL>(self.invFun.comp self.toFun).Homotopic (ContinuousMap.id X)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₕ Y<GOAL>⇑h.toFun = ↑h
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₕ Y<GOAL>Continuous ↑h
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>↑h.toHomotopyEquiv = ⇑h
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₕ Y<GOAL>⇑h.invFun = ↑h.symm
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>a : X<GOAL>↑(ContinuousMap.HomotopyEquiv.refl X) a = a
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>a : X<GOAL>↑(ContinuousMap.HomotopyEquiv.refl X).symm a = a
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>h₁ : X ≃ₕ Y<VAR>h₂ : Y ≃ₕ Z<GOAL>∀ (a : X), ↑(h₁.trans h₂) a = ↑h₂ (↑h₁ a)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>h₁ : X ≃ₕ Y<VAR>h₂ : Y ≃ₕ Z<GOAL>∀ (a : Z), ↑(h₁.trans h₂).symm a = ↑h₁.symm (↑h₂.symm a)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>h₁ : X ≃ₕ Y<VAR>h₂ : Y ≃ₕ Z<GOAL>(h₁.trans h₂).symm = h₂.symm.trans h₁.symm
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>(Homeomorph.refl X).toHomotopyEquiv = ContinuousMap.HomotopyEquiv.refl X
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>h.symm.toHomotopyEquiv = h.toHomotopyEquiv.symm
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>h₀ : X ≃ₜ Y<VAR>h₁ : Y ≃ₜ Z<GOAL>(h₀.trans h₁).toHomotopyEquiv = h₀.toHomotopyEquiv.trans h₁.toHomotopyEquiv
<VAR>α : Type u_1<VAR>t : TopologicalSpace α<VAR>Preorder α<VAR>self : OrderTopology α<GOAL>t = TopologicalSpace.generateFrom {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderTopology α<VAR>s : Set α<GOAL>IsOpen s ↔ TopologicalSpace.GenerateOpen {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a} s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>a : α<GOAL>IsOpen {b | a < b}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>a : α<GOAL>IsOpen {b | b < a}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>a b : α<VAR>h : a < b<GOAL>∀ᶠ (x : α) in 𝓝 b, a < x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>a b : α<VAR>h : a < b<GOAL>∀ᶠ (x : α) in 𝓝 b, a ≤ x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>a b : α<VAR>h : a < b<GOAL>∀ᶠ (x : α) in 𝓝 a, x < b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>a b : α<VAR>h : a < b<GOAL>∀ᶠ (x : α) in 𝓝 a, x ≤ b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>a : α<GOAL>𝓝 a = (⨅ b ∈ Set.Iio a, 𝓟 (Set.Ioi b)) ⊓ ⨅ b ∈ Set.Ioi a, 𝓟 (Set.Iio b)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>f : β → α<VAR>a : α<VAR>x : Filter β<GOAL>Filter.Tendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>f g h : β → α<VAR>b : Filter β<VAR>a : α<VAR>hg : Filter.Tendsto g b (𝓝 a)<VAR>hh : Filter.Tendsto h b (𝓝 a)<VAR>hgf : ∀ᶠ (b : β) in b, g b ≤ f b<VAR>hfh : ∀ᶠ (b : β) in b, f b ≤ h b<GOAL>Filter.Tendsto f b (𝓝 a)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>f g h : β → α<VAR>b : Filter β<VAR>a : α<VAR>hg : Filter.Tendsto g b (𝓝 a)<VAR>hh : Filter.Tendsto h b (𝓝 a)<VAR>hgf : g ≤ f<VAR>hfh : f ≤ h<GOAL>Filter.Tendsto f b (𝓝 a)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>a : α<VAR>hu : ∃ u, a < u<VAR>hl : ∃ l, l < a<GOAL>𝓝 a = ⨅ l, ⨅ (_ : l < a), ⨅ u, ⨅ (_ : a < u), 𝓟 (Set.Ioo l u)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>f : β → α<VAR>a : α<VAR>x : Filter β<VAR>hu : ∃ u, a < u<VAR>hl : ∃ l, l < a<VAR>h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u<GOAL>Filter.Tendsto f x (𝓝 a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<GOAL>TopologicalSpace.induced f inst✝ ≤ Preorder.topology α
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y<VAR>H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b<GOAL>TopologicalSpace.induced f inst✝ = Preorder.topology α
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>ta : TopologicalSpace β<VAR>Preorder β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>H₁ : ∀ {a : α} {x : β}, x < f a → ∃ b < a, x ≤ f b<VAR>H₂ : ∀ {a : α} {x : β}, f a < x → ∃ b > a, f b ≤ x<GOAL>OrderTopology α
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>ta : TopologicalSpace β<VAR>Preorder β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>H : ∀ {x y : β}, x < y → ∃ a, x < f a ∧ f a < y<GOAL>OrderTopology α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>LinearOrder β<VAR>t : TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>hc : (Set.range f).OrdConnected<GOAL>TopologicalSpace.induced f t = Preorder.topology α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>LinearOrder β<VAR>TopologicalSpace α<VAR>h : OrderTopology α<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>hc : (Set.range f).OrdConnected<GOAL>Embedding f
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>a : α<GOAL>𝓝[≥] a = (⨅ u, ⨅ (_ : a < u), 𝓟 (Set.Iio u)) ⊓ 𝓟 (Set.Ici a)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>a : α<GOAL>𝓝[≤] a = (⨅ l, ⨅ (_ : l < a), 𝓟 (Set.Ioi l)) ⊓ 𝓟 (Set.Iic a)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>a : α<VAR>ha : ∃ u, a < u<GOAL>𝓝[≥] a = ⨅ u, ⨅ (_ : a < u), 𝓟 (Set.Ico a u)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTopology α<VAR>a : α<VAR>ha : ∃ l, l < a<GOAL>𝓝[≤] a = ⨅ l, ⨅ (_ : l < a), 𝓟 (Set.Ioc l a)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>ha : ∃ u, a < u<GOAL>(𝓝[≥] a).HasBasis (fun u => a < u) fun u => Set.Ico a u
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>ha : ∃ l, l < a<GOAL>(𝓝[≤] a).HasBasis (fun l => l < a) fun l => Set.Ioc l a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>a : α<GOAL>(𝓝[≥] a).HasBasis (fun u => a < u) fun u => Set.Ico a u
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMinOrder α<VAR>a : α<GOAL>(𝓝[≤] a).HasBasis (fun l => l < a) fun l => Set.Ioc l a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderTop α<VAR>OrderTopology α<GOAL>𝓝 ⊤ = ⨅ l, ⨅ (_ : l < ⊤), 𝓟 (Set.Ioi l)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderBot α<VAR>OrderTopology α<GOAL>𝓝 ⊥ = ⨅ l, ⨅ (_ : ⊥ < l), 𝓟 (Set.Iio l)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTop α<VAR>OrderTopology α<VAR>Nontrivial α<GOAL>(𝓝 ⊤).HasBasis (fun a => a < ⊤) fun a => Set.Ioi a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderBot α<VAR>OrderTopology α<VAR>Nontrivial α<GOAL>(𝓝 ⊥).HasBasis (fun a => ⊥ < a) fun a => Set.Iio a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTop α<VAR>OrderTopology α<VAR>Nontrivial α<VAR>DenselyOrdered α<GOAL>(𝓝 ⊤).HasBasis (fun a => a < ⊤) Set.Ici
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderBot α<VAR>OrderTopology α<VAR>Nontrivial α<VAR>DenselyOrdered α<GOAL>(𝓝 ⊥).HasBasis (fun a => ⊥ < a) Set.Iic
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace β<VAR>Preorder β<VAR>OrderTop β<VAR>OrderTopology β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : Filter.Tendsto f l (𝓝 ⊤)<VAR>hg : f ≤ᶠ[l] g<GOAL>Filter.Tendsto g l (𝓝 ⊤)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace β<VAR>Preorder β<VAR>OrderBot β<VAR>OrderTopology β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : Filter.Tendsto f l (𝓝 ⊥)<VAR>hg : g ≤ᶠ[l] f<GOAL>Filter.Tendsto g l (𝓝 ⊥)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace β<VAR>Preorder β<VAR>OrderTop β<VAR>OrderTopology β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : Filter.Tendsto f l (𝓝 ⊤)<VAR>hg : f ≤ g<GOAL>Filter.Tendsto g l (𝓝 ⊤)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace β<VAR>Preorder β<VAR>OrderBot β<VAR>OrderTopology β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : Filter.Tendsto f l (𝓝 ⊥)<VAR>hg : g ≤ f<GOAL>Filter.Tendsto g l (𝓝 ⊥)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a₁ a₂ : α<VAR>h : a₁ < a₂<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ a₁ ∈ u ∧ a₂ ∈ v ∧ ∀ b₁ ∈ u, ∀ b₂ ∈ v, b₁ < b₂
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝 a<VAR>h : ∃ l, l < a<GOAL>∃ l < a, Set.Ioc l a ⊆ s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝 a<VAR>l : α<VAR>hl : l < a<GOAL>∃ l' ∈ Set.Ico l a, Set.Ioc l' a ⊆ s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝 a<VAR>u : α<VAR>hu : a < u<GOAL>∃ u' ∈ Set.Ioc a u, Set.Ico a u' ⊆ s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝 a<VAR>h : ∃ u, a < u<GOAL>∃ u, a < u ∧ Set.Ico a u ⊆ s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝[≥] a<GOAL>∃ b, a ≤ b ∧ Set.Icc a b ∈ 𝓝[≥] a ∧ Set.Icc a b ⊆ s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝[≤] a<GOAL>∃ b ≤ a, Set.Icc b a ∈ 𝓝[≤] a ∧ Set.Icc b a ⊆ s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝 a<GOAL>∃ b c, a ∈ Set.Icc b c ∧ Set.Icc b c ∈ 𝓝 a ∧ Set.Icc b c ⊆ s