ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type ua<VAR>UniformSpace α<VAR>a b : α<GOAL>𝓝 (a, b) = (𝓤 α).lift' fun s => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ s}
<VAR>α : Type ua<VAR>UniformSpace α<VAR>d : Set (α × α)<VAR>s : Set (α × α)<VAR>hd : d ∈ 𝓤 α<GOAL>∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<GOAL>𝓝 (x, x) ≤ 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>⨆ x, 𝓝 (x, x) ≤ 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>𝓝ˢ (Set.diagonal α) ≤ 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set (α × α)<GOAL>closure s = ⋂ V ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}, V ○ s ○ V
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>(𝓤 α).HasBasis (fun V => V ∈ 𝓤 α ∧ IsClosed V) id
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>𝓤 α = (𝓤 α).lift' closure
<VAR>α : Type ua<VAR>ι : Sort u_1<VAR>UniformSpace α<VAR>p : ι → Prop<VAR>U : ι → Set (α × α)<VAR>h : (𝓤 α).HasBasis p U<GOAL>(𝓤 α).HasBasis p fun i => closure (U i)
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>(𝓤 α).HasBasis (fun V => V ∈ 𝓤 α) closure
<VAR>α : Type ua<VAR>UniformSpace α<VAR>t : Set (α × α)<GOAL>closure t = ⋂ d ∈ 𝓤 α, d ○ (t ○ d)
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>𝓤 α = (𝓤 α).lift' interior
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>interior s ∈ 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set (α × α)<VAR>h : s ∈ 𝓤 α<GOAL>∃ t ∈ 𝓤 α, IsClosed t ∧ t ⊆ s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set α<GOAL>IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen V ∧ UniformSpace.ball x V ⊆ s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set α<VAR>U : Set (α × α)<VAR>hs : Dense s<VAR>hU : U ∈ 𝓤 α<GOAL>⋃ x ∈ s, UniformSpace.ball x U = Set.univ
<VAR>α : Type ua<VAR>UniformSpace α<VAR>ι : Type u_2<VAR>xs : ι → α<VAR>xs_dense : DenseRange xs<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<GOAL>⋃ i, UniformSpace.ball (xs i) U = Set.univ
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>(𝓤 α).HasBasis (fun V => V ∈ 𝓤 α ∧ IsOpen V) id
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>p : β → Prop<VAR>s : β → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<VAR>t : Set (α × α)<GOAL>t ∈ 𝓤 α ↔ ∃ i, p i ∧ ∀ (a b : α), (a, b) ∈ s i → (a, b) ∈ t
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>(𝓤 α).HasBasis (fun V => V ∈ 𝓤 α ∧ IsOpen V ∧ SymmetricRel V) id
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∃ t ∈ 𝓤 α, IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>(𝓤 α).IsCountablyGenerated<GOAL>∃ V, (𝓤 α).HasAntitoneBasis V ∧ ∀ (n : ℕ), SymmetricRel (V n)
<VAR>α : Type ua<VAR>ι : Sort u_1<VAR>UniformSpace α<VAR>p : ι → Prop<VAR>U : ι → Set (α × α)<VAR>h : (𝓤 α).HasBasis p U<VAR>s : Set α<GOAL>⋂ i, ⋂ (_ : p i), ⋃ x ∈ s, UniformSpace.ball x (U i) = closure s
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<GOAL>UniformContinuous f ↔ ∀ r ∈ 𝓤 β, {x | (f x.1, f x.2) ∈ r} ∈ 𝓤 α
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<GOAL>UniformContinuous f ↔ ∀ r ∈ 𝓤 β, ∀ᶠ (x : α × α) in 𝓤 α, (f x.1, f x.2) ∈ r
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<GOAL>UniformContinuousOn f Set.univ ↔ UniformContinuous f
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<VAR>c : α → β<VAR>h : ∀ (a b : α), c a = c b<GOAL>UniformContinuous c
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>UniformContinuous id
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<VAR>b : β<GOAL>UniformContinuous fun x => b
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : UniformContinuous g<VAR>hf : UniformContinuous f<GOAL>UniformContinuous (g ∘ f)
<VAR>β : Type ub<VAR>UniformSpace β<VAR>T : β → β<VAR>n : ℕ<VAR>h : UniformContinuous T<GOAL>UniformContinuous T^[n]
<VAR>α : Type ua<VAR>β : Type ub<VAR>ι : Sort u_1<VAR>UniformSpace α<VAR>ι' : Sort u_2<VAR>UniformSpace β<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>ha : (𝓤 α).HasBasis p s<VAR>q : ι' → Prop<VAR>t : ι' → Set (β × β)<VAR>hb : (𝓤 β).HasBasis q t<VAR>f : α → β<GOAL>UniformContinuous f ↔ ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ t i
<VAR>α : Type ua<VAR>β : Type ub<VAR>ι : Sort u_1<VAR>UniformSpace α<VAR>ι' : Sort u_2<VAR>UniformSpace β<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>ha : (𝓤 α).HasBasis p s<VAR>q : ι' → Prop<VAR>t : ι' → Set (β × β)<VAR>hb : (𝓤 β).HasBasis q t<VAR>f : α → β<VAR>S : Set α<GOAL>UniformContinuousOn f S ↔ ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i
<VAR>α : Type ua<VAR>u₁ u₂ : UniformSpace α<GOAL>u₁ ≤ u₂ ↔ 𝓤 α ≤ 𝓤 α
<VAR>α : Type ua<VAR>tt : Set (UniformSpace α)<VAR>t : UniformSpace α<VAR>h : t ∈ tt<GOAL>sInf tt ≤ t
<VAR>α : Type ua<VAR>tt : Set (UniformSpace α)<VAR>t : UniformSpace α<VAR>h : ∀ t' ∈ tt, t ≤ t'<GOAL>t ≤ sInf tt
<VAR>α : Type ua<VAR>ι : Sort u_2<VAR>u : ι → UniformSpace α<GOAL>𝓤 α = ⨅ i, 𝓤 α
<VAR>α : Type ua<VAR>u v : UniformSpace α<GOAL>𝓤 α = 𝓤 α ⊓ 𝓤 α
<VAR>α : Type ua<GOAL>𝓤 α = 𝓟 idRel
<VAR>α : Type ua<GOAL>𝓤 α = ⊤
<VAR>α : Type ua<VAR>β : Type ub<GOAL>∀ {x : UniformSpace β} (f : α → β), 𝓤 α = Filter.comap (Prod.map f f) (𝓤 β)
<VAR>α : Type u_2<GOAL>UniformSpace.comap id = id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>uγ : UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<GOAL>UniformSpace.comap (g ∘ f) uγ = UniformSpace.comap f (UniformSpace.comap g uγ)
<VAR>α : Type u_2<VAR>γ : Type u_3<VAR>u₁ u₂ : UniformSpace γ<VAR>f : α → γ<GOAL>UniformSpace.comap f (u₁ ⊓ u₂) = UniformSpace.comap f u₁ ⊓ UniformSpace.comap f u₂
<VAR>ι : Sort u_2<VAR>α : Type u_3<VAR>γ : Type u_4<VAR>u : ι → UniformSpace γ<VAR>f : α → γ<GOAL>UniformSpace.comap f (⨅ i, u i) = ⨅ i, UniformSpace.comap f (u i)
<VAR>α : Type u_2<VAR>γ : Type u_3<VAR>f : α → γ<GOAL>Monotone fun u => UniformSpace.comap f u
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>f : α → β<GOAL>UniformContinuous f ↔ uα ≤ UniformSpace.comap f uβ
<VAR>α : Type ua<VAR>u v : UniformSpace α<GOAL>u ≤ v ↔ UniformContinuous id
<VAR>α : Type ua<VAR>β : Type ub<VAR>f : α → β<VAR>u : UniformSpace β<GOAL>UniformContinuous f
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>f : γ → β<VAR>g : α → γ<VAR>v : UniformSpace β<VAR>u : UniformSpace α<VAR>h : UniformContinuous (f ∘ g)<GOAL>UniformContinuous g
<VAR>α : Type ua<VAR>u₁ u₂ : UniformSpace α<VAR>h : u₁ ≤ u₂<VAR>a : α<GOAL>𝓝 a ≤ 𝓝 a
<VAR>α : Type ua<VAR>u₁ u₂ : UniformSpace α<VAR>h : u₁ ≤ u₂<GOAL>UniformSpace.toTopologicalSpace ≤ UniformSpace.toTopologicalSpace
<VAR>α : Type ua<VAR>β : Type ub<VAR>f : α → β<VAR>u : UniformSpace β<GOAL>UniformSpace.toTopologicalSpace = TopologicalSpace.induced f UniformSpace.toTopologicalSpace
<VAR>α : Type ua<VAR>u : UniformSpace α<GOAL>u = ⊥ ↔ idRel ∈ 𝓤 α
<VAR>α : Type ua<VAR>ι : Sort u_2<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>u : UniformSpace α<VAR>h : (𝓤 α).HasBasis p s<GOAL>u = ⊥ ↔ ∃ i, p i ∧ Pairwise fun x y => (x, y) ∉ s i
<VAR>α : Type ua<GOAL>UniformSpace.toTopologicalSpace = ⊥
<VAR>α : Type ua<GOAL>UniformSpace.toTopologicalSpace = ⊤
<VAR>α : Type ua<VAR>ι : Sort u_2<VAR>u : ι → UniformSpace α<GOAL>UniformSpace.toTopologicalSpace = ⨅ i, UniformSpace.toTopologicalSpace
<VAR>α : Type ua<VAR>s : Set (UniformSpace α)<GOAL>UniformSpace.toTopologicalSpace = ⨅ i ∈ s, UniformSpace.toTopologicalSpace
<VAR>α : Type ua<VAR>u v : UniformSpace α<GOAL>UniformSpace.toTopologicalSpace = UniformSpace.toTopologicalSpace ⊓ UniformSpace.toTopologicalSpace
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>hf : UniformContinuous f<GOAL>Continuous f
<VAR>α : Type ua<VAR>β : Type ub<VAR>f : α → β<VAR>u₁ : UniformSpace α<VAR>u₂ u₃ : UniformSpace β<VAR>h₁ : UniformContinuous f<VAR>h₂ : UniformContinuous f<GOAL>UniformContinuous f
<VAR>α : Type ua<VAR>β : Type ub<VAR>f : α → β<VAR>u₁ u₂ : UniformSpace α<VAR>u₃ : UniformSpace β<VAR>hf : UniformContinuous f<GOAL>UniformContinuous f
<VAR>α : Type ua<VAR>β : Type ub<VAR>f : α → β<VAR>u₁ : Set (UniformSpace α)<VAR>u₂ : UniformSpace β<VAR>u : UniformSpace α<VAR>h₁ : u ∈ u₁<VAR>hf : UniformContinuous f<GOAL>UniformContinuous f
<VAR>α : Type ua<VAR>β : Type ub<VAR>f : α → β<VAR>u₁ : UniformSpace α<VAR>u₂ : Set (UniformSpace β)<GOAL>UniformContinuous f ↔ ∀ u ∈ u₂, UniformContinuous f
<VAR>α : Type ua<VAR>β : Type ub<VAR>ι : Sort u_1<VAR>f : α → β<VAR>u₁ : ι → UniformSpace α<VAR>u₂ : UniformSpace β<VAR>i : ι<VAR>hf : UniformContinuous f<GOAL>UniformContinuous f
<VAR>α : Type ua<VAR>β : Type ub<VAR>ι : Sort u_1<VAR>f : α → β<VAR>u₁ : UniformSpace α<VAR>u₂ : ι → UniformSpace β<GOAL>UniformContinuous f ↔ ∀ (i : ι), UniformContinuous f
<VAR>α : Type ua<VAR>hα : UniformSpace α<VAR>h : 𝓤 α = 𝓟 idRel<GOAL>DiscreteTopology α
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>UniformContinuous ⇑Additive.ofMul
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>UniformContinuous ⇑Additive.toMul
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>UniformContinuous ⇑Multiplicative.ofAdd
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>UniformContinuous ⇑Multiplicative.toAdd
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>𝓤 (Additive α) = Filter.map (Prod.map ⇑Additive.ofMul ⇑Additive.ofMul) (𝓤 α)
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>𝓤 (Multiplicative α) = Filter.map (Prod.map ⇑Multiplicative.ofAdd ⇑Multiplicative.ofAdd) (𝓤 α)
<VAR>α : Type ua<VAR>p : α → Prop<VAR>UniformSpace α<GOAL>𝓤 (Subtype p) = Filter.comap (fun q => (↑q.1, ↑q.2)) (𝓤 α)
<VAR>α : Type ua<VAR>s : Set α<VAR>UniformSpace α<GOAL>𝓤 ↑s = Filter.comap (Prod.map Subtype.val Subtype.val) (𝓤 α)
<VAR>α : Type ua<VAR>s : Set α<VAR>UniformSpace α<GOAL>Filter.map (Prod.map Subtype.val Subtype.val) (𝓤 ↑s) = 𝓤 α ⊓ 𝓟 (s ×ˢ s)
<VAR>α : Type ua<VAR>p : α → Prop<VAR>UniformSpace α<GOAL>UniformContinuous Subtype.val
<VAR>α : Type ua<VAR>β : Type ub<VAR>p : α → Prop<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<VAR>h : ∀ (x : β), p (f x)<GOAL>UniformContinuous fun x => ⟨f x, ⋯⟩
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>UniformContinuousOn f s ↔ UniformContinuous (s.restrict f)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : UniformContinuous fun x => f ↑x<VAR>ha : s ∈ 𝓝 a<GOAL>Filter.Tendsto f (𝓝 a) (𝓝 (f a))
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>h : UniformContinuousOn f s<GOAL>ContinuousOn f s
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>𝓤 αᵃᵒᵖ = Filter.comap (fun q => (AddOpposite.unop q.1, AddOpposite.unop q.2)) (𝓤 α)
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>𝓤 αᵐᵒᵖ = Filter.comap (fun q => (MulOpposite.unop q.1, MulOpposite.unop q.2)) (𝓤 α)
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>Filter.comap (fun p => (AddOpposite.op p.1, AddOpposite.op p.2)) (𝓤 αᵃᵒᵖ) = 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>Filter.comap (fun p => (MulOpposite.op p.1, MulOpposite.op p.2)) (𝓤 αᵐᵒᵖ) = 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>UniformContinuous MulOpposite.unop
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>UniformContinuous AddOpposite.unop
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>UniformContinuous MulOpposite.op
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>UniformContinuous AddOpposite.op
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>𝓤 (α × β) = Filter.comap (fun p => (p.1.1, p.2.1)) (𝓤 α) ⊓ Filter.comap (fun p => (p.1.2, p.2.2)) (𝓤 β)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>𝓤 (α × β) = Filter.comap (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>𝓤 (α × β) = Filter.map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<VAR>s : Set (β × β)<VAR>f : α → α → β<VAR>hf : UniformContinuous fun p => f p.1 p.2<VAR>hs : s ∈ 𝓤 β<GOAL>∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>t₁ : UniformSpace α<VAR>t₂ : UniformSpace β<VAR>a : Set (α × α)<VAR>b : Set (β × β)<VAR>ha : a ∈ 𝓤 α<VAR>hb : b ∈ 𝓤 β<GOAL>{p | (p.1.1, p.2.1) ∈ a ∧ (p.1.2, p.2.2) ∈ b} ∈ 𝓤 (α × β)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>Filter.Tendsto (fun p => (p.1.1, p.2.1)) (𝓤 (α × β)) (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>Filter.Tendsto (fun p => (p.1.2, p.2.2)) (𝓤 (α × β)) (𝓤 β)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>UniformContinuous fun p => p.1
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>UniformContinuous fun p => p.2
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f₁ : α → β<VAR>f₂ : α → γ<VAR>h₁ : UniformContinuous f₁<VAR>h₂ : UniformContinuous f₂<GOAL>UniformContinuous fun a => (f₁ a, f₂ a)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : α × β → γ<VAR>h : UniformContinuous f<VAR>b : β<GOAL>UniformContinuous fun a => f (a, b)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : α × β → γ<VAR>h : UniformContinuous f<VAR>a : α<GOAL>UniformContinuous fun b => f (a, b)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>UniformSpace δ<VAR>f : α → γ<VAR>g : β → δ<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<GOAL>UniformContinuous (Prod.map f g)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>u : UniformSpace α<VAR>v : UniformSpace β<GOAL>UniformSpace.toTopologicalSpace = instTopologicalSpaceProd
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : α → β → γ<VAR>ua1 ua2 : UniformSpace α<VAR>ub1 ub2 : UniformSpace β<VAR>uc1 : UniformSpace γ<VAR>h : UniformContinuous fun p => f p.1 p.2<GOAL>UniformContinuous fun p => f p.1 p.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : α → β → γ<VAR>uas : Set (UniformSpace α)<VAR>ubs : Set (UniformSpace β)<VAR>ua : UniformSpace α<VAR>ub : UniformSpace β<VAR>uc : UniformSpace γ<VAR>ha : ua ∈ uas<VAR>hb : ub ∈ ubs<VAR>hf : UniformContinuous fun p => f p.1 p.2<GOAL>UniformContinuous fun p => f p.1 p.2
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : α → β → γ<GOAL>UniformContinuous₂ f ↔ UniformContinuous (Function.uncurry f)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : α → β → γ<VAR>h : UniformContinuous₂ f<GOAL>UniformContinuous (Function.uncurry f)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : α × β → γ<GOAL>UniformContinuous₂ (Function.curry f) ↔ UniformContinuous f
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>UniformSpace δ<VAR>f : α → β → γ<VAR>g : γ → δ<VAR>hg : UniformContinuous g<VAR>hf : UniformContinuous₂ f<GOAL>UniformContinuous₂ (Function.bicompr g f)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>δ' : Type u_2<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>UniformSpace δ<VAR>UniformSpace δ'<VAR>f : α → β → γ<VAR>ga : δ → α<VAR>gb : δ' → β<VAR>hf : UniformContinuous₂ f<VAR>hga : UniformContinuous ga<VAR>hgb : UniformContinuous gb<GOAL>UniformContinuous₂ (Function.bicompl f ga gb)
<VAR>α : Type ua<VAR>u : UniformSpace α<VAR>p : α → Prop<GOAL>UniformSpace.toTopologicalSpace = instTopologicalSpaceSubtype
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<VAR>a : Set (α × α)<VAR>ha : a ∈ 𝓤 α<VAR>b : Set (β × β)<VAR>hb : b ∈ 𝓤 β<GOAL>Prod.map Sum.inl Sum.inl '' a ∪ Prod.map Sum.inr Sum.inr '' b ∈ 𝓤 (α ⊕ β)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>𝓤 (α ⊕ β) = Filter.map (Prod.map Sum.inl Sum.inl) (𝓤 α) ⊔ Filter.map (Prod.map Sum.inr Sum.inr) (𝓤 β)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>UniformContinuous Sum.inl
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>UniformContinuous Sum.inr
<VAR>α : Type ua<VAR>UniformSpace α<VAR>K : Set α<VAR>ι : Sort u_2<VAR>U : ι → Set α<VAR>hK : IsCompact K<VAR>hopen : ∀ (i : ι), IsOpen (U i)<VAR>hcover : K ⊆ ⋃ i, U i<GOAL>∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ i, UniformSpace.ball x V ⊆ U i
<VAR>α : Type ua<VAR>UniformSpace α<VAR>K : Set α<VAR>ι' : Sort u_2<VAR>ι : Sort u_3<VAR>p : ι' → Prop<VAR>V : ι' → Set (α × α)<VAR>U : ι → Set α<VAR>hbasis : (𝓤 α).HasBasis p V<VAR>hK : IsCompact K<VAR>hopen : ∀ (j : ι), IsOpen (U j)<VAR>hcover : K ⊆ ⋃ j, U j<GOAL>∃ i, p i ∧ ∀ x ∈ K, ∃ j, UniformSpace.ball x (V i) ⊆ U j
<VAR>α : Type ua<VAR>UniformSpace α<VAR>K : Set α<VAR>S : Set (Set α)<VAR>hK : IsCompact K<VAR>hopen : ∀ s ∈ S, IsOpen s<VAR>hcover : K ⊆ ⋃₀ S<GOAL>∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, UniformSpace.ball x V ⊆ s
<VAR>α : Type ua<VAR>ι : Sort u_1<VAR>UniformSpace α<VAR>K : Set α<VAR>p : ι → Prop<VAR>V : ι → Set (α × α)<VAR>hbasis : (𝓤 α).HasBasis p V<VAR>hK : IsCompact K<GOAL>(𝓝ˢ K).HasBasis p fun i => ⋃ x ∈ K, UniformSpace.ball x (V i)
<VAR>α : Type ua<VAR>UniformSpace α<VAR>A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<GOAL>∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, UniformSpace.ball x V) (⋃ x ∈ B, UniformSpace.ball x V)
<VAR>α : Type ua<VAR>ι : Sort u_1<VAR>UniformSpace α<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>hU : (𝓤 α).HasBasis p s<VAR>A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<GOAL>∃ i, p i ∧ Disjoint (⋃ x ∈ A, UniformSpace.ball x (s i)) (⋃ x ∈ B, UniformSpace.ball x (s i))
<VAR>α : Type ua<VAR>UniformSpace α<VAR>K U : Set α<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∃ V ∈ 𝓤 α, IsOpen V ∧ ∀ x ∈ K, UniformSpace.ball x V ⊆ U
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>Filter.Tendsto u f (𝓝 a) ↔ Filter.Tendsto (fun x => (a, u x)) f (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>Filter.Tendsto u f (𝓝 a) ↔ Filter.Tendsto (fun x => (u x, a)) f (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<GOAL>ContinuousAt f b ↔ Filter.Tendsto (fun x => (f b, f x)) (𝓝 b) (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<GOAL>ContinuousAt f b ↔ Filter.Tendsto (fun x => (f x, f b)) (𝓝 b) (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<GOAL>ContinuousAt f b ↔ Filter.Tendsto (fun x => (f x.1, f x.2)) (𝓝 (b, b)) (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>s : Set β<GOAL>ContinuousWithinAt f s b ↔ Filter.Tendsto (fun x => (f b, f x)) (𝓝[s] b) (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>s : Set β<GOAL>ContinuousWithinAt f s b ↔ Filter.Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>s : Set β<GOAL>ContinuousOn f s ↔ ∀ b ∈ s, Filter.Tendsto (fun x => (f b, f x)) (𝓝[s] b) (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>s : Set β<GOAL>ContinuousOn f s ↔ ∀ b ∈ s, Filter.Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>TopologicalSpace β<VAR>f : β → α<GOAL>Continuous f ↔ ∀ (b : β), Filter.Tendsto (fun x => (f b, f x)) (𝓝 b) (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>TopologicalSpace β<VAR>f : β → α<GOAL>Continuous f ↔ ∀ (b : β), Filter.Tendsto (fun x => (f x, f b)) (𝓝 b) (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>TopologicalSpace β<VAR>r : Set (α × α)<VAR>s : Set β<VAR>f g : β → α<VAR>hf : ∀ x ∈ s, ContinuousAt f x<VAR>hg : ∀ x ∈ s, ContinuousAt g x<VAR>hfg : Set.EqOn f g s<VAR>hr : r ∈ 𝓤 α<GOAL>∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>UniformSpace β<VAR>f g : α → β<VAR>l : Filter α<VAR>b : β<VAR>hf : Filter.Tendsto f l (𝓝 b)<VAR>hg : Filter.Tendsto (fun x => (f x, g x)) l (𝓤 β)<GOAL>Filter.Tendsto g l (𝓝 b)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>UniformSpace β<VAR>f g : α → β<VAR>l : Filter α<VAR>b : β<VAR>hfg : Filter.Tendsto (fun x => (f x, g x)) l (𝓤 β)<GOAL>Filter.Tendsto f l (𝓝 b) ↔ Filter.Tendsto g l (𝓝 b)
<VAR>α : Type u_3<VAR>h : TopologicalSpace α<VAR>self : PolishSpace α<GOAL>∃ m, UniformSpace.toTopologicalSpace = h ∧ CompleteSpace α
<VAR>α : Type u_3<VAR>ht : TopologicalSpace α<VAR>h : PolishSpace α<GOAL>CompleteSpace α
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>PolishSpace α<GOAL>T2Space α
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>PolishSpace α<VAR>Nonempty α<GOAL>∃ f, Continuous f ∧ Function.Surjective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>PolishSpace β<VAR>f : α → β<VAR>hf : ClosedEmbedding f<GOAL>PolishSpace α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>PolishSpace β<VAR>f : α ≃ β<GOAL>PolishSpace α
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>PolishSpace α<VAR>s : Set α<VAR>hs : IsClosed s<GOAL>PolishSpace ↑s
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Countable ι<VAR>t : ι → TopologicalSpace α<VAR>ht₀ : ∃ t₀, T2Space α ∧ ∀ (i : ι), t i ≤ t₀<VAR>ht : ∀ (i : ι), ∃ u, CompleteSpace α ∧ (𝓤 α).IsCountablyGenerated ∧ UniformSpace.toTopologicalSpace = t i<GOAL>∃ u, CompleteSpace α ∧ (𝓤 α).IsCountablyGenerated ∧ UniformSpace.toTopologicalSpace = ⨅ i, t i
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Countable ι<VAR>t : ι → TopologicalSpace α<VAR>ht₀ : ∃ i₀, ∀ (i : ι), t i ≤ t i₀<VAR>ht : ∀ (i : ι), PolishSpace α<GOAL>PolishSpace α
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Countable ι<VAR>t : TopologicalSpace α<VAR>p : PolishSpace α<VAR>m : ι → TopologicalSpace α<VAR>hm : ∀ (n : ι), m n ≤ t<VAR>h'm : ∀ (n : ι), PolishSpace α<GOAL>∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>s : TopologicalSpace.Opens α<VAR>x y : s.CompleteCopy<GOAL>dist x y = dist ↑x ↑y + |1 / Metric.infDist (↑x) (↑s)ᶜ - 1 / Metric.infDist (↑y) (↑s)ᶜ|
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>s : TopologicalSpace.Opens α<VAR>x y : s.CompleteCopy<GOAL>dist ↑x ↑y ≤ dist x y
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>PolishSpace α<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>PolishSpace ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>PolishSpace α<VAR>s : Set α<VAR>hs : IsClosed s<GOAL>PolishSpace.IsClopenable s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : PolishSpace.IsClopenable s<GOAL>PolishSpace.IsClopenable sᶜ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>PolishSpace α<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>PolishSpace.IsClopenable s
<VAR>α : Type u_1<VAR>t : TopologicalSpace α<VAR>PolishSpace α<VAR>s : ℕ → Set α<VAR>hs : ∀ (n : ℕ), PolishSpace.IsClopenable (s n)<GOAL>PolishSpace.IsClopenable (⋃ n, s n)
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>s t : Set X<VAR>h : IsMetricSeparated s t<GOAL>IsMetricSeparated t s
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>s t : Set X<GOAL>IsMetricSeparated s t ↔ IsMetricSeparated t s
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>s : Set X<GOAL>IsMetricSeparated ∅ s
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>s : Set X<GOAL>IsMetricSeparated s ∅
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>s t : Set X<VAR>h : IsMetricSeparated s t<GOAL>Disjoint s t
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>s t : Set X<VAR>h : IsMetricSeparated s t<GOAL>s ⊆ tᶜ
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>s t s' t' : Set X<VAR>hs : s ⊆ s'<VAR>ht : t ⊆ t'<GOAL>IsMetricSeparated s' t' → IsMetricSeparated s t
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>s t s' : Set X<VAR>h' : IsMetricSeparated s' t<VAR>hs : s ⊆ s'<GOAL>IsMetricSeparated s t
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>s t t' : Set X<VAR>h' : IsMetricSeparated s t'<VAR>ht : t ⊆ t'<GOAL>IsMetricSeparated s t
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>s t s' : Set X<VAR>h : IsMetricSeparated s t<VAR>h' : IsMetricSeparated s' t<GOAL>IsMetricSeparated (s ∪ s') t
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>s t s' : Set X<GOAL>IsMetricSeparated (s ∪ s') t ↔ IsMetricSeparated s t ∧ IsMetricSeparated s' t