ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>Nontrivial α<VAR>s : Set α<VAR>hs : IsOpen s<VAR>h : s.Nonempty<GOAL>∃ a b, a < b ∧ Set.Ioo a b ⊆ s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>Nontrivial α<VAR>s : Set α<VAR>h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, a < c ∧ c < b<GOAL>Dense s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>Nontrivial α<VAR>s : Set α<GOAL>Dense s ↔ ∀ (a b : α), a < b → ∃ c ∈ s, a < c ∧ c < b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hl : ∃ l, l < a<VAR>hu : ∃ u, a < u<GOAL>s ∈ 𝓝 a ↔ ∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>NoMinOrder α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ 𝓝 a ↔ ∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>hl : ∃ l, l < a<VAR>hu : ∃ u, a < u<GOAL>(𝓝 a).HasBasis (fun b => b.1 < a ∧ a < b.2) fun b => Set.Ioo b.1 b.2
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>NoMinOrder α<VAR>a : α<GOAL>(𝓝 a).HasBasis (fun b => b.1 < a ∧ a < b.2) fun b => Set.Ioo b.1 b.2
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>NoMinOrder α<VAR>a : α<VAR>p : α → Prop<VAR>hp : ∀ᶠ (x : α) in 𝓝 a, p x<GOAL>∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ {x | p x}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>s : Set α<VAR>hs : Dense s<GOAL>inst✝ = TopologicalSpace.generateFrom (Set.Ioi '' s ∪ Set.Iio '' s)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderBot α<GOAL>Filter.atBot ≤ 𝓝 ⊥
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTop α<GOAL>Filter.atTop ≤ 𝓝 ⊤
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>TopologicalSpace.SeparableSpace α<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<GOAL>{x | ∃ y, x ⋖ y}.Countable
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<GOAL>{x | ∃ y, y ⋖ x}.Countable
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<GOAL>{x | ∃ y < x, Set.Ioo y x = ∅}.Countable
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>SecondCountableTopology α<VAR>y : α → α<VAR>s : Set α<VAR>h : s.PairwiseDisjoint fun x => Set.Ioo x (y x)<VAR>h' : ∀ x ∈ s, x < y x<GOAL>s.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>f : β → α<VAR>SecondCountableTopology α<GOAL>{x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>f : β → α<VAR>SecondCountableTopology α<GOAL>{x | ∃ z < f x, ∀ (y : β), x < y → f y ≤ z}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>f : β → α<VAR>SecondCountableTopology α<GOAL>{x | ∃ z, f x < z ∧ ∀ y < x, z ≤ f y}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>f : β → α<VAR>SecondCountableTopology α<GOAL>{x | ∃ z < f x, ∀ y < x, f y ≤ z}.Countable
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>Finite ι<VAR>(i : ι) → LinearOrder (π i)<VAR>(i : ι) → TopologicalSpace (π i)<VAR>∀ (i : ι), OrderTopology (π i)<VAR>a x : (i : ι) → π i<VAR>ha : ∀ (i : ι), x i < a i<GOAL>Set.Iic a ∈ 𝓝 x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>ι : Type u_1<VAR>Finite ι<VAR>a' x' : ι → α<VAR>ha : ∀ (i : ι), x' i < a' i<GOAL>Set.Iic a' ∈ 𝓝 x'
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>Finite ι<VAR>(i : ι) → LinearOrder (π i)<VAR>(i : ι) → TopologicalSpace (π i)<VAR>∀ (i : ι), OrderTopology (π i)<VAR>a x : (i : ι) → π i<VAR>ha : ∀ (i : ι), a i < x i<GOAL>Set.Ici a ∈ 𝓝 x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>ι : Type u_1<VAR>Finite ι<VAR>a' x' : ι → α<VAR>ha : ∀ (i : ι), a' i < x' i<GOAL>Set.Ici a' ∈ 𝓝 x'
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>Finite ι<VAR>(i : ι) → LinearOrder (π i)<VAR>(i : ι) → TopologicalSpace (π i)<VAR>∀ (i : ι), OrderTopology (π i)<VAR>a b x : (i : ι) → π i<VAR>ha : ∀ (i : ι), a i < x i<VAR>hb : ∀ (i : ι), x i < b i<GOAL>Set.Icc a b ∈ 𝓝 x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>ι : Type u_1<VAR>Finite ι<VAR>a' b' x' : ι → α<VAR>ha : ∀ (i : ι), a' i < x' i<VAR>hb : ∀ (i : ι), x' i < b' i<GOAL>Set.Icc a' b' ∈ 𝓝 x'
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>Finite ι<VAR>(i : ι) → LinearOrder (π i)<VAR>(i : ι) → TopologicalSpace (π i)<VAR>∀ (i : ι), OrderTopology (π i)<VAR>a x : (i : ι) → π i<VAR>Nonempty ι<VAR>ha : ∀ (i : ι), x i < a i<GOAL>Set.Iio a ∈ 𝓝 x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>ι : Type u_1<VAR>Finite ι<VAR>a' x' : ι → α<VAR>Nonempty ι<VAR>ha : ∀ (i : ι), x' i < a' i<GOAL>Set.Iio a' ∈ 𝓝 x'
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>Finite ι<VAR>(i : ι) → LinearOrder (π i)<VAR>(i : ι) → TopologicalSpace (π i)<VAR>∀ (i : ι), OrderTopology (π i)<VAR>a x : (i : ι) → π i<VAR>Nonempty ι<VAR>ha : ∀ (i : ι), a i < x i<GOAL>Set.Ioi a ∈ 𝓝 x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>ι : Type u_1<VAR>Finite ι<VAR>a' x' : ι → α<VAR>Nonempty ι<VAR>ha : ∀ (i : ι), a' i < x' i<GOAL>Set.Ioi a' ∈ 𝓝 x'
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>Finite ι<VAR>(i : ι) → LinearOrder (π i)<VAR>(i : ι) → TopologicalSpace (π i)<VAR>∀ (i : ι), OrderTopology (π i)<VAR>a b x : (i : ι) → π i<VAR>Nonempty ι<VAR>ha : ∀ (i : ι), a i < x i<VAR>hb : ∀ (i : ι), x i < b i<GOAL>Set.Ioc a b ∈ 𝓝 x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>ι : Type u_1<VAR>Finite ι<VAR>a' b' x' : ι → α<VAR>Nonempty ι<VAR>ha : ∀ (i : ι), a' i < x' i<VAR>hb : ∀ (i : ι), x' i < b' i<GOAL>Set.Ioc a' b' ∈ 𝓝 x'
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>Finite ι<VAR>(i : ι) → LinearOrder (π i)<VAR>(i : ι) → TopologicalSpace (π i)<VAR>∀ (i : ι), OrderTopology (π i)<VAR>a b x : (i : ι) → π i<VAR>Nonempty ι<VAR>ha : ∀ (i : ι), a i < x i<VAR>hb : ∀ (i : ι), x i < b i<GOAL>Set.Ico a b ∈ 𝓝 x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>ι : Type u_1<VAR>Finite ι<VAR>a' b' x' : ι → α<VAR>Nonempty ι<VAR>ha : ∀ (i : ι), a' i < x' i<VAR>hb : ∀ (i : ι), x' i < b' i<GOAL>Set.Ico a' b' ∈ 𝓝 x'
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>Finite ι<VAR>(i : ι) → LinearOrder (π i)<VAR>(i : ι) → TopologicalSpace (π i)<VAR>∀ (i : ι), OrderTopology (π i)<VAR>a b x : (i : ι) → π i<VAR>Nonempty ι<VAR>ha : ∀ (i : ι), a i < x i<VAR>hb : ∀ (i : ι), x i < b i<GOAL>Set.Ioo a b ∈ 𝓝 x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>ι : Type u_1<VAR>Finite ι<VAR>a' b' x' : ι → α<VAR>Nonempty ι<VAR>ha : ∀ (i : ι), a' i < x' i<VAR>hb : ∀ (i : ι), x' i < b' i<GOAL>Set.Ioo a' b' ∈ 𝓝 x'
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>C : Set α<VAR>x : α<VAR>U : Set α<VAR>h_acc : AccPt x (𝓟 C)<VAR>hU : U ∈ 𝓝 x<GOAL>AccPt x (𝓟 (U ∩ C))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>C : Set α<GOAL>Perfect C ↔ IsClosed C ∧ Preperfect C
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>C : Set α<VAR>self : Perfect C<GOAL>IsClosed C
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>C : Set α<VAR>self : Perfect C<GOAL>Preperfect C
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>C : Set α<GOAL>Preperfect C ↔ ∀ x ∈ C, ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>PerfectSpace α ↔ Preperfect Set.univ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>self : PerfectSpace α<GOAL>Preperfect Set.univ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>PerfectSpace α<GOAL>Perfect Set.univ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>C U : Set α<VAR>hC : Preperfect C<VAR>hU : IsOpen U<GOAL>Preperfect (U ∩ C)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>C : Set α<VAR>hC : Preperfect C<GOAL>Perfect (closure C)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>C : Set α<VAR>T1Space α<GOAL>Preperfect C ↔ Perfect (closure C)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>C U : Set α<VAR>hC : Perfect C<VAR>x : α<VAR>xC : x ∈ C<VAR>xU : x ∈ U<VAR>Uop : IsOpen U<GOAL>Perfect (closure (U ∩ C)) ∧ (closure (U ∩ C)).Nonempty
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>C : Set α<VAR>T25Space α<VAR>hC : Perfect C<VAR>hnonempty : C.Nonempty<GOAL>∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>T1Space α<VAR>U : Set α<VAR>hu : U.Nontrivial<VAR>h : IsPreconnected U<GOAL>Preperfect U
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>C : Set α<VAR>SecondCountableTopology α<VAR>hclosed : IsClosed C<GOAL>∃ V D, V.Countable ∧ Perfect D ∧ C = V ∪ D
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>C : Set α<VAR>SecondCountableTopology α<VAR>hclosed : IsClosed C<VAR>hunc : ¬C.Countable<GOAL>∃ D, Perfect D ∧ D.Nonempty ∧ D ⊆ C
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>PerfectSpace X ↔ ∀ (x : X), (𝓝[≠] x).NeBot
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>Inducing f
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Inducing id
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : Inducing g<VAR>hf : Inducing f<GOAL>Inducing (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : Inducing g<GOAL>Inducing (g ∘ f) ↔ Inducing f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : Inducing (g ∘ f)<GOAL>Inducing f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Inducing f ↔ ∀ (x : X), 𝓝 x = Filter.comap f (𝓝 (f x))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<VAR>x : X<GOAL>𝓝 x = Filter.comap f (𝓝 (f x))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_4<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>p : ι → Prop<VAR>s : ι → Set Y<VAR>hf : Inducing f<VAR>x : X<VAR>h_basis : (𝓝 (f x)).HasBasis p s<GOAL>(𝓝 x).HasBasis p (Set.preimage f ∘ s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<VAR>s : Set X<GOAL>𝓝ˢ s = Filter.comap f (𝓝ˢ (f '' s))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<VAR>x : X<GOAL>Filter.map f (𝓝 x) = 𝓝[Set.range f] f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<VAR>x : X<VAR>h : Set.range f ∈ 𝓝 (f x)<GOAL>Filter.map f (𝓝 x) = 𝓝 (f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<VAR>x : X<VAR>l : Filter X<GOAL>MapClusterPt (f x) l f ↔ ClusterPt x l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<VAR>x : X<VAR>s : Set X<VAR>hs : s ∈ 𝓝 x<GOAL>f '' s ∈ 𝓝[Set.range f] f x
<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>g : Y → Z<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : ι → Y<VAR>l : Filter ι<VAR>y : Y<VAR>hg : Inducing g<GOAL>Filter.Tendsto f l (𝓝 y) ↔ Filter.Tendsto (g ∘ f) l (𝓝 (g y))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : Inducing g<VAR>x : X<GOAL>ContinuousAt f x ↔ ContinuousAt (g ∘ f) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : Inducing g<GOAL>Continuous f ↔ Continuous (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hf : Inducing f<VAR>x : X<VAR>h : Set.range f ∈ 𝓝 (f x)<GOAL>ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<GOAL>Continuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<VAR>s : Set X<GOAL>closure s = f ⁻¹' closure (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<VAR>s : Set X<GOAL>IsClosed s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<VAR>s : Set X<GOAL>IsClosed s ↔ ∀ (x : X), f x ∈ closure (f '' s) → x ∈ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : Inducing f<VAR>s : Set Y<VAR>hs : IsClosed s<GOAL>IsClosed (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<VAR>s : Set X<GOAL>IsOpen s ↔ ∃ t, IsOpen t ∧ f ⁻¹' t = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<GOAL>{s | IsOpen s} = Set.preimage f '' {t | IsOpen t}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<VAR>s : Set X<GOAL>Dense s ↔ ∀ (x : X), f x ∈ closure (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Subsingleton X<VAR>f : X → Y<GOAL>Inducing f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>t : TopologicalSpace Y<VAR>hf : Function.Injective f<GOAL>Embedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>inj : Function.Injective f<VAR>induced : ∀ (x : X), Filter.comap f (𝓝 (f x)) = 𝓝 x<GOAL>Embedding f
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Embedding id
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : Embedding g<VAR>hf : Embedding f<GOAL>Embedding (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : Embedding g<GOAL>Embedding (g ∘ f) ↔ Embedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : Embedding (g ∘ f)<GOAL>Embedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>g : Y → X<VAR>h : Function.LeftInverse f g<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Embedding g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Embedding f<VAR>x : X<GOAL>Filter.map f (𝓝 x) = 𝓝[Set.range f] f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Embedding f<VAR>x : X<VAR>h : Set.range f ∈ 𝓝 (f x)<GOAL>Filter.map f (𝓝 x) = 𝓝 (f x)
<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>g : Y → Z<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : ι → Y<VAR>l : Filter ι<VAR>y : Y<VAR>hg : Embedding g<GOAL>Filter.Tendsto f l (𝓝 y) ↔ Filter.Tendsto (g ∘ f) l (𝓝 (g y))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : Embedding g<GOAL>Continuous f ↔ Continuous (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Embedding f<GOAL>Continuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Embedding f<VAR>s : Set X<GOAL>closure s = f ⁻¹' closure (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>DiscreteTopology Y<VAR>hf : Embedding f<GOAL>DiscreteTopology X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Subsingleton X<VAR>f : X → Y<GOAL>Embedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>QuotientMap f ↔ Function.Surjective f ∧ ∀ (s : Set Y), IsOpen s ↔ IsOpen (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>QuotientMap f ↔ Function.Surjective f ∧ ∀ (s : Set Y), IsClosed s ↔ IsClosed (f ⁻¹' s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>QuotientMap id
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : QuotientMap g<VAR>hf : QuotientMap f<GOAL>QuotientMap (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : QuotientMap (g ∘ f)<GOAL>QuotientMap g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>g : Y → X<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Function.LeftInverse g f<GOAL>QuotientMap g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hf : QuotientMap f<GOAL>Continuous g ↔ Continuous (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : QuotientMap f<GOAL>Continuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : QuotientMap f<GOAL>Function.Surjective f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : QuotientMap f<VAR>s : Set Y<GOAL>IsOpen (f ⁻¹' s) ↔ IsOpen s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : QuotientMap f<VAR>s : Set Y<GOAL>IsClosed (f ⁻¹' s) ↔ IsClosed s
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>IsOpenMap id
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : IsOpenMap g<VAR>hf : IsOpenMap f<GOAL>IsOpenMap (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : IsOpenMap f<GOAL>IsOpen (Set.range f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : IsOpenMap f<VAR>x : X<VAR>s : Set X<VAR>hx : s ∈ 𝓝 x<GOAL>f '' s ∈ 𝓝 (f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : IsOpenMap f<VAR>x : X<GOAL>Set.range f ∈ 𝓝 (f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : IsOpenMap f<VAR>s : Set X<VAR>t : Set Y<VAR>h : Set.MapsTo f s t<GOAL>Set.MapsTo f (interior s) (interior t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : IsOpenMap f<VAR>s : Set X<GOAL>f '' interior s ⊆ interior (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : IsOpenMap f<VAR>x : X<GOAL>𝓝 (f x) ≤ Filter.map f (𝓝 x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : ∀ (x : X), 𝓝 (f x) ≤ Filter.map f (𝓝 x)<GOAL>IsOpenMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : ∀ (x : X), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ Function.RightInverse g f<GOAL>IsOpenMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f' : Y → X<VAR>h : Continuous f'<VAR>l_inv : Function.LeftInverse f f'<VAR>r_inv : Function.RightInverse f f'<GOAL>IsOpenMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>open_map : IsOpenMap f<VAR>cont : Continuous f<VAR>surj : Function.Surjective f<GOAL>QuotientMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : IsOpenMap f<VAR>s : Set Y<GOAL>interior (f ⁻¹' s) ⊆ f ⁻¹' interior s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf₁ : IsOpenMap f<VAR>hf₂ : Continuous f<VAR>s : Set Y<GOAL>f ⁻¹' interior s = interior (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : IsOpenMap f<VAR>s : Set Y<GOAL>f ⁻¹' closure s ⊆ closure (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : IsOpenMap f<VAR>hfc : Continuous f<VAR>s : Set Y<GOAL>f ⁻¹' closure s = closure (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : IsOpenMap f<VAR>s : Set Y<GOAL>f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : IsOpenMap f<VAR>hfc : Continuous f<VAR>s : Set Y<GOAL>f ⁻¹' frontier s = frontier (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : IsEmpty X<VAR>f : X → Y<GOAL>IsOpenMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsOpenMap f ↔ ∀ (x : X), 𝓝 (f x) ≤ Filter.map f (𝓝 x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsOpenMap f ↔ ∀ (s : Set X), f '' interior s ⊆ interior (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hi : Inducing f<VAR>ho : IsOpen (Set.range f)<GOAL>IsOpenMap f
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>IsClosedMap id
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : IsClosedMap g<VAR>hf : IsClosedMap f<GOAL>IsClosedMap (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : IsClosedMap f<VAR>s : Set X<GOAL>closure (f '' s) ⊆ f '' closure s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f' : Y → X<VAR>h : Continuous f'<VAR>l_inv : Function.LeftInverse f f'<VAR>r_inv : Function.RightInverse f f'<GOAL>IsClosedMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : ∀ (s : Set X), IsClosed s → s.Nonempty → IsClosed (f '' s)<GOAL>IsClosedMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : IsClosedMap f<GOAL>IsClosed (Set.range f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hcl : IsClosedMap f<VAR>hcont : Continuous f<VAR>hsurj : Function.Surjective f<GOAL>QuotientMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Inducing f<VAR>h : IsClosed (Set.range f)<GOAL>IsClosedMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsClosedMap f ↔ ∀ (s : Set X), closure (f '' s) ⊆ f '' closure s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsClosedMap f ↔ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f_closed : IsClosedMap f<VAR>f_cont : Continuous f<VAR>s : Set X<GOAL>closure (f '' s) = f '' closure s