ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>A B : DiscreteQuotient X<VAR>h : A ≤ B<GOAL>DiscreteQuotient.ofLE h ∘ A.proj = B.proj
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>LocallyConnectedSpace X<VAR>x y : X<GOAL>⊥.proj x = ⊥.proj y ↔ connectedComponent x = connectedComponent y
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>DiscreteTopology X<VAR>x y : X<GOAL>⊥.proj x = ⊥.proj y ↔ x = y
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>DiscreteTopology X<GOAL>Function.Injective ⊥.proj
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>DiscreteTopology X<GOAL>Function.Bijective ⊥.proj
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>A : DiscreteQuotient X<GOAL>DiscreteQuotient.LEComap (ContinuousMap.id X) A A
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>A A' : DiscreteQuotient X<GOAL>DiscreteQuotient.LEComap (ContinuousMap.id X) A A' ↔ A ≤ A'
<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>f : C(X, Y)<VAR>A : DiscreteQuotient X<VAR>B : DiscreteQuotient Y<VAR>g : C(Y, Z)<VAR>C : DiscreteQuotient Z<GOAL>DiscreteQuotient.LEComap g B C → DiscreteQuotient.LEComap f A B → DiscreteQuotient.LEComap (g.comp f) A C
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>A A' : DiscreteQuotient X<VAR>B B' : DiscreteQuotient Y<VAR>h : DiscreteQuotient.LEComap f A B<VAR>hA : A' ≤ A<VAR>hB : B ≤ B'<GOAL>DiscreteQuotient.LEComap f A' B'
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>A : DiscreteQuotient X<VAR>B : DiscreteQuotient Y<VAR>cond : DiscreteQuotient.LEComap f A B<GOAL>Continuous (DiscreteQuotient.map f cond)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>A : DiscreteQuotient X<VAR>B : DiscreteQuotient Y<VAR>cond : DiscreteQuotient.LEComap f A B<GOAL>DiscreteQuotient.map f cond ∘ A.proj = B.proj ∘ ⇑f
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>A : DiscreteQuotient X<VAR>B : DiscreteQuotient Y<VAR>cond : DiscreteQuotient.LEComap f A B<VAR>x : X<GOAL>DiscreteQuotient.map f cond (A.proj x) = B.proj (f x)
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>A : DiscreteQuotient X<GOAL>DiscreteQuotient.map (ContinuousMap.id X) ⋯ = id
<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>f : C(X, Y)<VAR>A : DiscreteQuotient X<VAR>B : DiscreteQuotient Y<VAR>g : C(Y, Z)<VAR>C : DiscreteQuotient Z<VAR>h1 : DiscreteQuotient.LEComap g B C<VAR>h2 : DiscreteQuotient.LEComap f A B<GOAL>DiscreteQuotient.map (g.comp f) ⋯ = DiscreteQuotient.map g h1 ∘ DiscreteQuotient.map f h2
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>A : DiscreteQuotient X<VAR>B B' : DiscreteQuotient Y<VAR>cond : DiscreteQuotient.LEComap f A B<VAR>h : B ≤ B'<VAR>a : Quotient A.toSetoid<GOAL>DiscreteQuotient.ofLE h (DiscreteQuotient.map f cond a) = DiscreteQuotient.map f ⋯ a
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>A : DiscreteQuotient X<VAR>B B' : DiscreteQuotient Y<VAR>cond : DiscreteQuotient.LEComap f A B<VAR>h : B ≤ B'<GOAL>DiscreteQuotient.ofLE h ∘ DiscreteQuotient.map f cond = DiscreteQuotient.map f ⋯
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>A A' : DiscreteQuotient X<VAR>B : DiscreteQuotient Y<VAR>cond : DiscreteQuotient.LEComap f A B<VAR>h : A' ≤ A<VAR>c : Quotient A'.toSetoid<GOAL>DiscreteQuotient.map f cond (DiscreteQuotient.ofLE h c) = DiscreteQuotient.map f ⋯ c
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>A A' : DiscreteQuotient X<VAR>B : DiscreteQuotient Y<VAR>cond : DiscreteQuotient.LEComap f A B<VAR>h : A' ≤ A<GOAL>DiscreteQuotient.map f cond ∘ DiscreteQuotient.ofLE h = DiscreteQuotient.map f ⋯
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>T2Space X<VAR>CompactSpace X<VAR>disc : TotallyDisconnectedSpace X<VAR>x y : X<VAR>h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y<GOAL>x = y
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>A B : DiscreteQuotient X<VAR>h : A ≤ B<VAR>a : Quotient A.toSetoid<GOAL>A.proj ⁻¹' {a} ⊆ B.proj ⁻¹' {DiscreteQuotient.ofLE h a}
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid<VAR>compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), DiscreteQuotient.ofLE h (Qs A) = Qs B<GOAL>∃ x, ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>CompactSpace X<GOAL>((Set.image fun t => t.carrier) ∘ Finset.toSet) ∘ DiscreteQuotient.finsetClopens X = fun x => match x with | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>CompactSpace X<GOAL>Function.Injective (DiscreteQuotient.finsetClopens X)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>f : LocallyConstant X α<GOAL>⇑f.lift ∘ f.discreteQuotient.proj = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>self : IsSpectralMap f<VAR>s : Set β<GOAL>IsOpen s → IsCompact s → IsCompact (f ⁻¹' s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>hf : IsSpectralMap f<VAR>h₀ : IsCompact s<VAR>h₁ : IsOpen s<GOAL>IsCompact (f ⁻¹' s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : IsSpectralMap f<GOAL>Continuous f
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>IsSpectralMap id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : β → γ<VAR>g : α → β<VAR>hf : IsSpectralMap f<VAR>hg : IsSpectralMap g<GOAL>IsSpectralMap (f ∘ g)
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>self : SpectralMap α β<GOAL>IsSpectralMap self.toFun
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>FunLike F α β<VAR>self : SpectralMapClass F α β<VAR>f : F<GOAL>IsSpectralMap ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : SpectralMap α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f g : SpectralMap α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : SpectralMap α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : SpectralMap α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>⇑(SpectralMap.id α) = id
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>a : α<GOAL>(SpectralMap.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : SpectralMap β γ<VAR>g : SpectralMap α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : SpectralMap β γ<VAR>g : SpectralMap α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : SpectralMap β γ<VAR>g : SpectralMap α β<GOAL>⇑f ∘ ⇑g = ⇑↑f ∘ ⇑↑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : SpectralMap β γ<VAR>g : SpectralMap α β<GOAL>↑(f.comp g) = (↑f).comp ↑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>f : SpectralMap γ δ<VAR>g : SpectralMap β γ<VAR>h : SpectralMap α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : SpectralMap α β<GOAL>f.comp (SpectralMap.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : SpectralMap α β<GOAL>(SpectralMap.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g₁ g₂ : SpectralMap β γ<VAR>f : SpectralMap α β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g : SpectralMap β γ<VAR>f₁ f₂ : SpectralMap α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>X : Type v<VAR>TopologicalSpace X<VAR>self : ParacompactSpace X<VAR>α : Type v<VAR>s : α → Set X<GOAL>(∀ (a : α), IsOpen (s a)) → ⋃ a, s a = Set.univ → ∃ β t, (∀ (b : β), IsOpen (t b)) ∧ ⋃ b, t b = Set.univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>ParacompactSpace X<VAR>u : ι → Set X<VAR>uo : ∀ (a : ι), IsOpen (u a)<VAR>uc : ⋃ i, u i = Set.univ<GOAL>∃ v, (∀ (a : ι), IsOpen (v a)) ∧ ⋃ i, v i = Set.univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>ParacompactSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>u : ι → Set X<VAR>uo : ∀ (i : ι), IsOpen (u i)<VAR>us : s ⊆ ⋃ i, u i<GOAL>∃ v, (∀ (i : ι), IsOpen (v i)) ∧ s ⊆ ⋃ i, v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
<VAR>X : Type v<VAR>Y : Type w<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>ParacompactSpace Y<VAR>e : X → Y<VAR>he : ClosedEmbedding e<GOAL>ParacompactSpace X
<VAR>X : Type v<VAR>Y : Type w<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<GOAL>ParacompactSpace X ↔ ParacompactSpace Y
<VAR>X : Type v<VAR>TopologicalSpace X<VAR>WeaklyLocallyCompactSpace X<VAR>SigmaCompactSpace X<VAR>T2Space X<VAR>ι : X → Type u<VAR>p : (x : X) → ι x → Prop<VAR>B : (x : X) → ι x → Set X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hB : ∀ x ∈ s, (𝓝 x).HasBasis (p x) (B x)<GOAL>∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ a, B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
<VAR>X : Type v<VAR>TopologicalSpace X<VAR>WeaklyLocallyCompactSpace X<VAR>SigmaCompactSpace X<VAR>T2Space X<VAR>ι : X → Type u<VAR>p : (x : X) → ι x → Prop<VAR>B : (x : X) → ι x → Set X<VAR>hB : ∀ (x : X), (𝓝 x).HasBasis (p x) (B x)<GOAL>∃ α c r, (∀ (a : α), p (c a) (r a)) ∧ ⋃ a, B (c a) (r a) = Set.univ ∧ LocallyFinite fun a => B (c a) (r a)
<VAR>X : Type u_3<VAR>TopologicalSpace (X × X)<GOAL>𝓝ˢ (Set.diagonal X) = ⨆ x, 𝓝 (x, x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>s ∈ 𝓝ˢ t ↔ ∀ x ∈ t, s ∈ 𝓝 x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>f : Filter X<VAR>s : Set X<GOAL>𝓝ˢ s ≤ f ↔ ∀ x ∈ s, 𝓝 x ≤ f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>t : X → Set X<VAR>h : ∀ x ∈ s, t x ∈ 𝓝 x<GOAL>⋃ x ∈ s, t x ∈ 𝓝ˢ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>s ⊆ interior t ↔ t ∈ 𝓝ˢ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure s) t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>s ∈ 𝓝ˢ t ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>p : X → Prop<GOAL>(∀ᶠ (x : X) in 𝓝ˢ s, p x) ↔ ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, p x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>p : X → Prop<GOAL>(∀ᶠ (x : X) in 𝓝ˢ s, p x) ↔ ∀ x ∈ s, ∀ᶠ (y : X) in 𝓝 x, p y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>(𝓝ˢ s).HasBasis (fun U => IsOpen U ∧ s ⊆ U) fun U => U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>(𝓝ˢ s).lift' interior = 𝓝ˢ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>t : Set X<VAR>h : (𝓝ˢ t).HasBasis p s<GOAL>(𝓝ˢ t).HasBasis p fun x => interior (s x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hU : IsOpen s<GOAL>s ∈ 𝓝ˢ t ↔ t ⊆ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ho : IsOpen s<GOAL>s ∈ 𝓝ˢ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>𝓟 s ≤ 𝓝ˢ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>h : t ∈ 𝓝ˢ s<GOAL>s ⊆ t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>p : X → Prop<VAR>h : ∀ᶠ (x : X) in 𝓝ˢ s, p x<VAR>x : X<GOAL>x ∈ s → p x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f g : X → Y<VAR>h : f =ᶠ[𝓝ˢ s] g<GOAL>Set.EqOn f g s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>𝓝ˢ s = 𝓟 s ↔ IsOpen s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>𝓝ˢ (interior s) = 𝓟 (interior s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>𝓝ˢ {x} = 𝓝 x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ∈ 𝓝ˢ (interior s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>𝓝ˢ ∅ = ⊥
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ∈ 𝓝ˢ ∅
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>𝓝ˢ Set.univ = ⊤
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>h : s ⊆ t<GOAL>𝓝ˢ s ≤ 𝓝ˢ t
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Monotone 𝓝ˢ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>x : X<VAR>h : x ∈ s<GOAL>𝓝 x ≤ 𝓝ˢ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s₁ s₂ t₁ t₂ : Set X<VAR>h₁ : s₁ ∈ 𝓝ˢ t₁<VAR>h₂ : s₂ ∈ 𝓝ˢ t₂<GOAL>s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<VAR>s : Set X<GOAL>𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<VAR>t : Set Y<VAR>hf : Continuous f<VAR>hst : Set.MapsTo f s t<GOAL>Filter.Tendsto f (𝓝ˢ s) (𝓝ˢ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>y : Y<VAR>f : X → Y<VAR>h : Continuous f<VAR>h' : Set.EqOn f (fun x => y) s<GOAL>Filter.Tendsto f (𝓝ˢ s) (𝓝 y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>𝓝ˢ (s ∩ t) ≤ 𝓝ˢ s ⊓ 𝓝ˢ t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>t : Set X<VAR>h : IsClosed t<GOAL>𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>t : Set X<VAR>h : IsClosed t<GOAL>𝓝ˢ s ≤ 𝓝ˢ (t ∩ s) ⊔ 𝓟 tᶜ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>p : X → Prop<VAR>h : ∀ᶠ (y : X) in 𝓝ˢ s, p y<GOAL>∀ᶠ (y : X) in 𝓝ˢ s, ∀ᶠ (x : X) in 𝓝 y, p x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>p : X → Prop<GOAL>(∀ᶠ (x : X) in 𝓝ˢ (s ∪ t), p x) ↔ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>p : X → Prop<VAR>hs : ∀ᶠ (x : X) in 𝓝ˢ s, p x<VAR>ht : ∀ᶠ (x : X) in 𝓝ˢ t, p x<GOAL>∀ᶠ (x : X) in 𝓝ˢ (s ∪ t), p x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : Sort u_3<VAR>s : ι → Set X<GOAL>𝓝ˢ (⋃ i, s i) = ⨆ i, 𝓝ˢ (s i)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>P : X → Prop<GOAL>(∀ᶠ (x : X) in 𝓝ˢ (⋃ i, ⋃ (_ : p i), s i), P x) ↔ ∀ (i : ι), p i → ∀ᶠ (x : X) in 𝓝ˢ (s i), P x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : Sort u_3<VAR>s : ι → Set X<VAR>P : X → Prop<GOAL>(∀ᶠ (x : X) in 𝓝ˢ (⋃ i, s i), P x) ↔ ∀ (i : ι), ∀ᶠ (x : X) in 𝓝ˢ (s i), P x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>h : Inducing f<GOAL>Inducing (s.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>h : Embedding f<GOAL>Embedding (s.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>h : OpenEmbedding f<GOAL>OpenEmbedding (s.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>h : ClosedEmbedding f<GOAL>ClosedEmbedding (s.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>H : IsClosedMap f<VAR>s : Set β<GOAL>IsClosedMap (s.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>H : IsClosedMap f<GOAL>IsClosedMap (s.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>H : IsOpenMap f<VAR>s : Set β<GOAL>IsOpenMap (s.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>H : IsOpenMap f<GOAL>IsOpenMap (s.restrictPreimage f)
<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>ι : Type u_3<VAR>U : ι → TopologicalSpace.Opens β<VAR>hU : iSup U = ⊤<VAR>s : Set β<GOAL>IsOpen s ↔ ∀ (i : ι), IsOpen (s ∩ ↑(U i))
<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>ι : Type u_3<VAR>U : ι → TopologicalSpace.Opens β<VAR>hU : iSup U = ⊤<VAR>s : Set β<GOAL>IsOpen s ↔ ∀ (i : ι), IsOpen (Subtype.val ⁻¹' s)
<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>ι : Type u_3<VAR>U : ι → TopologicalSpace.Opens β<VAR>hU : iSup U = ⊤<VAR>s : Set β<GOAL>IsClosed s ↔ ∀ (i : ι), IsClosed (Subtype.val ⁻¹' s)
<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>ι : Type u_3<VAR>U : ι → TopologicalSpace.Opens β<VAR>hU : iSup U = ⊤<VAR>s : Set β<GOAL>IsLocallyClosed s ↔ ∀ (i : ι), IsLocallyClosed (Subtype.val ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>ι : Type u_3<VAR>U : ι → TopologicalSpace.Opens β<VAR>hU : iSup U = ⊤<GOAL>IsOpenMap f ↔ ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>ι : Type u_3<VAR>U : ι → TopologicalSpace.Opens β<VAR>hU : iSup U = ⊤<GOAL>IsClosedMap f ↔ ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>ι : Type u_3<VAR>U : ι → TopologicalSpace.Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>Inducing f ↔ ∀ (i : ι), Inducing ((U i).carrier.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>ι : Type u_3<VAR>U : ι → TopologicalSpace.Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>Embedding f ↔ ∀ (i : ι), Embedding ((U i).carrier.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>ι : Type u_3<VAR>U : ι → TopologicalSpace.Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>OpenEmbedding f ↔ ∀ (i : ι), OpenEmbedding ((U i).carrier.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>ι : Type u_3<VAR>U : ι → TopologicalSpace.Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>ClosedEmbedding f ↔ ∀ (i : ι), ClosedEmbedding ((U i).carrier.restrictPreimage f)
<VAR>α : Type u_2<VAR>f : Filter α<VAR>m : α → ℝ<VAR>a : ℝ<GOAL>Filter.Tendsto (fun a => ↑(m a)) f (𝓝 ↑a) ↔ Filter.Tendsto m f (𝓝 a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<GOAL>(Continuous fun a => ↑(f a)) ↔ Continuous f
<VAR>r : ℝ<GOAL>𝓝 ↑r = Filter.map Real.toEReal (𝓝 r)
<VAR>r p : ℝ<GOAL>𝓝 (↑r, ↑p) = Filter.map (fun p => (↑p.1, ↑p.2)) (𝓝 (r, p))
<VAR>a : EReal<VAR>ha : a ≠ ⊤<VAR>h'a : a ≠ ⊥<GOAL>Filter.Tendsto EReal.toReal (𝓝 a) (𝓝 a.toReal)
<GOAL>ContinuousOn EReal.toReal {⊥, ⊤}ᶜ
<VAR>α : Type u_2<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>Filter.Tendsto (fun a => ↑(m a)) f (𝓝 ↑a) ↔ Filter.Tendsto m f (𝓝 a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ≥0∞<GOAL>(Continuous fun a => ↑(f a)) ↔ Continuous f
<GOAL>𝓝 ⊤ = ⨅ a, ⨅ (_ : a ≠ ⊤), 𝓟 (Set.Ioi a)
<GOAL>(𝓝 ⊤).HasBasis (fun x => True) fun x => Set.Ioi ↑x
<GOAL>𝓝 ⊤ = ⨅ a, 𝓟 (Set.Ioi ↑a)
<VAR>s : Set EReal<GOAL>s ∈ 𝓝 ⊤ ↔ ∃ y, Set.Ioi ↑y ⊆ s
<VAR>α : Type u_2<VAR>m : α → EReal<VAR>f : Filter α<GOAL>Filter.Tendsto m f (𝓝 ⊤) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, ↑x < m a
<GOAL>𝓝 ⊥ = ⨅ a, ⨅ (_ : a ≠ ⊥), 𝓟 (Set.Iio a)
<GOAL>(𝓝 ⊥).HasBasis (fun x => True) fun x => Set.Iio ↑x
<GOAL>𝓝 ⊥ = ⨅ a, 𝓟 (Set.Iio ↑a)
<VAR>s : Set EReal<GOAL>s ∈ 𝓝 ⊥ ↔ ∃ y, Set.Iio ↑y ⊆ s
<VAR>α : Type u_2<VAR>m : α → EReal<VAR>f : Filter α<GOAL>Filter.Tendsto m f (𝓝 ⊥) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, m a < ↑x
<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>h : u ≤ᶠ[f] v<GOAL>Filter.liminf u f ≤ Filter.liminf v f
<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>h : u ≤ᶠ[f] v<GOAL>Filter.limsup u f ≤ Filter.limsup v f
<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : Filter.limsup u f < a<VAR>hb : Filter.limsup v f < b<GOAL>Filter.limsup (u + v) f ≤ a + b
<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : Filter.limsup u f < a<VAR>hb : Filter.limsup v f < b<GOAL>Filter.limsup (u + v) f < a + b
<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>h : Filter.limsup u f = ⊥<VAR>h' : Filter.limsup v f ≠ ⊤<GOAL>Filter.limsup (u + v) f = ⊥
<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>h : Filter.limsup u f ≠ ⊥ ∨ Filter.limsup v f ≠ ⊤<VAR>h' : Filter.limsup u f ≠ ⊤ ∨ Filter.limsup v f ≠ ⊥<GOAL>Filter.limsup (u + v) f ≤ Filter.limsup u f + Filter.limsup v f
<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : Filter.limsup u f < a<VAR>hb : Filter.limsup v f ≤ b<GOAL>Filter.limsup (u + v) f ≤ a + b
<VAR>α : Type u_2<VAR>f : Filter α<VAR>v : α → EReal<GOAL>Filter.liminf (-v) f = -Filter.limsup v f
<VAR>α : Type u_2<VAR>f : Filter α<VAR>v : α → EReal<GOAL>Filter.limsup (-v) f = -Filter.liminf v f
<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : a < Filter.liminf u f<VAR>hb : b < Filter.liminf v f<GOAL>a + b < Filter.liminf (u + v) f
<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>h : Filter.liminf u f = ⊤<VAR>h' : Filter.liminf v f ≠ ⊥<GOAL>Filter.liminf (u + v) f = ⊤
<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<GOAL>Filter.liminf u f + Filter.liminf v f ≤ Filter.liminf (u + v) f
<VAR>α : Type u_2<VAR>f : Filter α<VAR>u : α → EReal<VAR>b : EReal<GOAL>Filter.limsup u f ≤ b ↔ ∀ (c : ℝ), b < ↑c → ∀ᶠ (a : α) in f, u a ≤ ↑c
<VAR>a b : ℝ<GOAL>ContinuousAt (fun p => p.1 + p.2) (↑a, ↑b)
<VAR>a : ℝ<GOAL>ContinuousAt (fun p => p.1 + p.2) (⊤, ↑a)
<VAR>a : ℝ<GOAL>ContinuousAt (fun p => p.1 + p.2) (↑a, ⊤)
<GOAL>ContinuousAt (fun p => p.1 + p.2) (⊤, ⊤)
<VAR>a : ℝ<GOAL>ContinuousAt (fun p => p.1 + p.2) (⊥, ↑a)
<VAR>a : ℝ<GOAL>ContinuousAt (fun p => p.1 + p.2) (↑a, ⊥)
<GOAL>ContinuousAt (fun p => p.1 + p.2) (⊥, ⊥)
<VAR>p : EReal × EReal<VAR>h : p.1 ≠ ⊤ ∨ p.2 ≠ ⊥<VAR>h' : p.1 ≠ ⊥ ∨ p.2 ≠ ⊤<GOAL>ContinuousAt (fun p => p.1 + p.2) p
<VAR>a b : EReal<VAR>h : ContinuousAt (fun p => p.1 * p.2) (a, b)<GOAL>ContinuousAt (fun p => p.1 * p.2) (b, a)
<VAR>a b : EReal<VAR>h : ContinuousAt (fun p => p.1 * p.2) (a, b)<GOAL>ContinuousAt (fun p => p.1 * p.2) (-a, b)
<VAR>a b : EReal<VAR>h : ContinuousAt (fun p => p.1 * p.2) (a, b)<GOAL>ContinuousAt (fun p => p.1 * p.2) (a, -b)
<VAR>a b : EReal<VAR>h : ContinuousAt (fun p => p.1 * p.2) (a, b)<GOAL>ContinuousAt (fun p => p.1 * p.2) (-a, -b)
<VAR>a b : ℝ<GOAL>ContinuousAt (fun p => p.1 * p.2) (↑a, ↑b)
<GOAL>ContinuousAt (fun p => p.1 * p.2) (⊤, ⊤)
<VAR>a : ℝ<VAR>h : 0 < a<GOAL>ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)
<VAR>a : ℝ<VAR>h : a ≠ 0<GOAL>ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)
<VAR>p : EReal × EReal<VAR>h₁ : p.1 ≠ 0 ∨ p.2 ≠ ⊥<VAR>h₂ : p.1 ≠ 0 ∨ p.2 ≠ ⊤<VAR>h₃ : p.1 ≠ ⊥ ∨ p.2 ≠ 0<VAR>h₄ : p.1 ≠ ⊤ ∨ p.2 ≠ 0<GOAL>ContinuousAt (fun p => p.1 * p.2) p
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<GOAL>IsLocalHomeomorphOn f s ↔ ∀ x ∈ s, ∃ U ∈ 𝓝 x, OpenEmbedding (U.restrict f)
<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>h : ∀ x ∈ s, ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source<GOAL>IsLocalHomeomorphOn f s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>IsLocalHomeomorphOn (↑e) e.source