ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>A : X → Matrix l n R<VAR>hA : Continuous A<VAR>e₁ : l ≃ m<VAR>e₂ : n ≃ p<GOAL>Continuous fun x => (Matrix.reindex e₁ e₂) (A x)
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>A : X → Matrix n n R<VAR>hA : Continuous A<GOAL>Continuous fun x => (A x).diag
<VAR>n : Type u_5<VAR>R : Type u_8<VAR>TopologicalSpace R<GOAL>Continuous Matrix.diag
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>Fintype n<VAR>AddCommMonoid R<VAR>ContinuousAdd R<VAR>A : X → Matrix n n R<VAR>hA : Continuous A<GOAL>Continuous fun x => (A x).trace
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing R<VAR>TopologicalRing R<VAR>A : X → Matrix n n R<VAR>hA : Continuous A<GOAL>Continuous fun x => (A x).det
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>DecidableEq n<VAR>i : n<VAR>A : X → Matrix m n R<VAR>B : X → m → R<VAR>hA : Continuous A<VAR>hB : Continuous B<GOAL>Continuous fun x => (A x).updateColumn i (B x)
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>DecidableEq m<VAR>i : m<VAR>A : X → Matrix m n R<VAR>B : X → n → R<VAR>hA : Continuous A<VAR>hB : Continuous B<GOAL>Continuous fun x => (A x).updateRow i (B x)
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing R<VAR>TopologicalRing R<VAR>A : X → Matrix n n R<VAR>B : X → n → R<VAR>hA : Continuous A<VAR>hB : Continuous B<GOAL>Continuous fun x => (A x).cramer (B x)
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing R<VAR>TopologicalRing R<VAR>A : X → Matrix n n R<VAR>hA : Continuous A<GOAL>Continuous fun x => (A x).adjugate
<VAR>n : Type u_5<VAR>R : Type u_8<VAR>TopologicalSpace R<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing R<VAR>TopologicalRing R<VAR>A : Matrix n n R<VAR>h : ContinuousAt Ring.inverse A.det<GOAL>ContinuousAt Inv.inv A
<VAR>X : Type u_1<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>A : X → Matrix n l R<VAR>B : X → Matrix n m R<VAR>C : X → Matrix p l R<VAR>D : X → Matrix p m R<VAR>hA : Continuous A<VAR>hB : Continuous B<VAR>hC : Continuous C<VAR>hD : Continuous D<GOAL>Continuous fun x => Matrix.fromBlocks (A x) (B x) (C x) (D x)
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>Zero R<VAR>DecidableEq p<VAR>A : X → p → Matrix m n R<VAR>hA : Continuous A<GOAL>Continuous fun x => Matrix.blockDiagonal (A x)
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>A : X → Matrix (m × p) (n × p) R<VAR>hA : Continuous A<GOAL>Continuous fun x => (A x).blockDiag
<VAR>X : Type u_1<VAR>l : Type u_3<VAR>R : Type u_8<VAR>m' : l → Type u_9<VAR>n' : l → Type u_10<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>Zero R<VAR>DecidableEq l<VAR>A : X → (i : l) → Matrix (m' i) (n' i) R<VAR>hA : Continuous A<GOAL>Continuous fun x => Matrix.blockDiagonal' (A x)
<VAR>X : Type u_1<VAR>l : Type u_3<VAR>R : Type u_8<VAR>m' : l → Type u_9<VAR>n' : l → Type u_10<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>A : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R<VAR>hA : Continuous A<GOAL>Continuous fun x => (A x).blockDiag'
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>f : X → Matrix m n R<VAR>a : Matrix m n R<VAR>hf : HasSum f a<GOAL>HasSum (fun x => (f x)ᵀ) aᵀ
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>f : X → Matrix m n R<VAR>hf : Summable f<GOAL>Summable fun x => (f x)ᵀ
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>f : X → Matrix m n R<GOAL>(Summable fun x => (f x)ᵀ) ↔ Summable f
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>T2Space R<VAR>f : X → Matrix m n R<GOAL>(∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>StarAddMonoid R<VAR>ContinuousStar R<VAR>f : X → Matrix m n R<VAR>a : Matrix m n R<VAR>hf : HasSum f a<GOAL>HasSum (fun x => (f x)ᴴ) aᴴ
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>StarAddMonoid R<VAR>ContinuousStar R<VAR>f : X → Matrix m n R<VAR>hf : Summable f<GOAL>Summable fun x => (f x)ᴴ
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>StarAddMonoid R<VAR>ContinuousStar R<VAR>f : X → Matrix m n R<GOAL>(Summable fun x => (f x)ᴴ) ↔ Summable f
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>StarAddMonoid R<VAR>ContinuousStar R<VAR>T2Space R<VAR>f : X → Matrix m n R<GOAL>(∑' (x : X), f x)ᴴ = ∑' (x : X), (f x)ᴴ
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>DecidableEq n<VAR>f : X → n → R<VAR>a : n → R<VAR>hf : HasSum f a<GOAL>HasSum (fun x => Matrix.diagonal (f x)) (Matrix.diagonal a)
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>DecidableEq n<VAR>f : X → n → R<VAR>hf : Summable f<GOAL>Summable fun x => Matrix.diagonal (f x)
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>DecidableEq n<VAR>f : X → n → R<GOAL>(Summable fun x => Matrix.diagonal (f x)) ↔ Summable f
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>DecidableEq n<VAR>T2Space R<VAR>f : X → n → R<GOAL>Matrix.diagonal (∑' (x : X), f x) = ∑' (x : X), Matrix.diagonal (f x)
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>f : X → Matrix n n R<VAR>a : Matrix n n R<VAR>hf : HasSum f a<GOAL>HasSum (fun x => (f x).diag) a.diag
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>f : X → Matrix n n R<VAR>hf : Summable f<GOAL>Summable fun x => (f x).diag
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>DecidableEq p<VAR>f : X → p → Matrix m n R<VAR>a : p → Matrix m n R<VAR>hf : HasSum f a<GOAL>HasSum (fun x => Matrix.blockDiagonal (f x)) (Matrix.blockDiagonal a)
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>DecidableEq p<VAR>f : X → p → Matrix m n R<VAR>hf : Summable f<GOAL>Summable fun x => Matrix.blockDiagonal (f x)
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>DecidableEq p<VAR>f : X → p → Matrix m n R<GOAL>(Summable fun x => Matrix.blockDiagonal (f x)) ↔ Summable f
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>DecidableEq p<VAR>T2Space R<VAR>f : X → p → Matrix m n R<GOAL>Matrix.blockDiagonal (∑' (x : X), f x) = ∑' (x : X), Matrix.blockDiagonal (f x)
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>f : X → Matrix (m × p) (n × p) R<VAR>a : Matrix (m × p) (n × p) R<VAR>hf : HasSum f a<GOAL>HasSum (fun x => (f x).blockDiag) a.blockDiag
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>R : Type u_8<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>f : X → Matrix (m × p) (n × p) R<VAR>hf : Summable f<GOAL>Summable fun x => (f x).blockDiag
<VAR>X : Type u_1<VAR>l : Type u_3<VAR>R : Type u_8<VAR>m' : l → Type u_9<VAR>n' : l → Type u_10<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>DecidableEq l<VAR>f : X → (i : l) → Matrix (m' i) (n' i) R<VAR>a : (i : l) → Matrix (m' i) (n' i) R<VAR>hf : HasSum f a<GOAL>HasSum (fun x => Matrix.blockDiagonal' (f x)) (Matrix.blockDiagonal' a)
<VAR>X : Type u_1<VAR>l : Type u_3<VAR>R : Type u_8<VAR>m' : l → Type u_9<VAR>n' : l → Type u_10<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>DecidableEq l<VAR>f : X → (i : l) → Matrix (m' i) (n' i) R<VAR>hf : Summable f<GOAL>Summable fun x => Matrix.blockDiagonal' (f x)
<VAR>X : Type u_1<VAR>l : Type u_3<VAR>R : Type u_8<VAR>m' : l → Type u_9<VAR>n' : l → Type u_10<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>DecidableEq l<VAR>f : X → (i : l) → Matrix (m' i) (n' i) R<GOAL>(Summable fun x => Matrix.blockDiagonal' (f x)) ↔ Summable f
<VAR>X : Type u_1<VAR>l : Type u_3<VAR>R : Type u_8<VAR>m' : l → Type u_9<VAR>n' : l → Type u_10<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>DecidableEq l<VAR>T2Space R<VAR>f : X → (i : l) → Matrix (m' i) (n' i) R<GOAL>Matrix.blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), Matrix.blockDiagonal' (f x)
<VAR>X : Type u_1<VAR>l : Type u_3<VAR>R : Type u_8<VAR>m' : l → Type u_9<VAR>n' : l → Type u_10<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>f : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R<VAR>a : Matrix ((i : l) × m' i) ((i : l) × n' i) R<VAR>hf : HasSum f a<GOAL>HasSum (fun x => (f x).blockDiag') a.blockDiag'
<VAR>X : Type u_1<VAR>l : Type u_3<VAR>R : Type u_8<VAR>m' : l → Type u_9<VAR>n' : l → Type u_10<VAR>AddCommMonoid R<VAR>TopologicalSpace R<VAR>f : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R<VAR>hf : Summable f<GOAL>Summable fun x => (f x).blockDiag'
<GOAL>TopologicalSpace.IsTopologicalBasis (⋃ a, ⋃ b, ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})
<GOAL>Bornology.cobounded ℝ = Filter.atBot ⊔ Filter.atTop
<VAR>s : Set ℝ<VAR>x : ℝ<GOAL>x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, |y - x| < ε
<VAR>s : Set ℝ<VAR>r : ℝ<VAR>r0 : 0 < r<VAR>H : ∀ x ∈ s, r ≤ |x|<GOAL>UniformContinuous fun p => (↑p)⁻¹
<VAR>x : ℝ<GOAL>UniformContinuous fun x_1 => x * x_1
<VAR>s : Set (ℝ × ℝ)<VAR>r₁ r₂ : ℝ<VAR>H : ∀ x ∈ s, |x.1| < r₁ ∧ |x.2| < r₂<GOAL>UniformContinuous fun p => (↑p).1 * (↑p).2
<VAR>x ε : ℝ<GOAL>TotallyBounded (Metric.ball x ε)
<VAR>q : ℚ<GOAL>closure (Rat.cast '' {x | q < x}) = {r | ↑q ≤ r}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>f : ℝ → α<VAR>c : ℝ<VAR>hp : Function.Periodic f c<VAR>hc : c ≠ 0<VAR>hf : Continuous f<GOAL>IsCompact (Set.range f)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>f : ℝ → α<VAR>c : ℝ<VAR>hp : Function.Periodic f c<VAR>hc : c ≠ 0<VAR>hf : Continuous f<GOAL>Bornology.IsBounded (Set.range f)
<GOAL>Filter.Tendsto Int.cast Filter.cofinite (Filter.cocompact ℝ)
<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>Filter.Tendsto (⇑((zmultiplesHom ℝ) a)) Filter.cofinite (Filter.cocompact ℝ)
<VAR>a : ℝ<GOAL>Filter.Tendsto (⇑(AddSubgroup.zmultiples a).subtype) Filter.cofinite (Filter.cocompact ℝ)
<VAR>s : Set ℚ<VAR>hs : IsCompact s<GOAL>interior s = ∅
<VAR>s : Set ℚ<VAR>hs : IsCompact s<GOAL>Dense sᶜ
<GOAL>¬(Filter.cocompact ℚ).IsCountablyGenerated
<GOAL>¬(𝓝 ∞).IsCountablyGenerated
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>self : ExtremallyDisconnected X<VAR>U : Set X<GOAL>IsOpen U → IsOpen (closure U)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>ExtremallyDisconnected X<VAR>e : X ≃ₜ Y<GOAL>ExtremallyDisconnected Y
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>DiscreteTopology X<GOAL>CompactT2.Projective (StoneCech X)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>h : CompactT2.Projective X<GOAL>ExtremallyDisconnected X
<VAR>A D : Type u<VAR>TopologicalSpace A<VAR>TopologicalSpace D<VAR>T1Space A<VAR>CompactSpace D<VAR>π : D → A<VAR>π_cont : Continuous π<VAR>π_surj : Function.Surjective π<GOAL>∃ E, CompactSpace ↑E ∧ π '' E = Set.univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ Set.univ → IsClosed E₀ → E.restrict π '' E₀ ≠ Set.univ
<VAR>A E : Type u<VAR>TopologicalSpace A<VAR>TopologicalSpace E<VAR>ρ : E → A<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Function.Surjective ρ<VAR>zorn_subset : ∀ (E₀ : Set E), E₀ ≠ Set.univ → IsClosed E₀ → ρ '' E₀ ≠ Set.univ<VAR>G : Set E<VAR>hG : IsOpen G<GOAL>ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ
<VAR>A : Type u<VAR>TopologicalSpace A<VAR>ExtremallyDisconnected A<VAR>U₁ U₂ : Set A<VAR>h : Disjoint U₁ U₂<VAR>hU₁ : IsOpen U₁<VAR>hU₂ : IsOpen U₂<GOAL>Disjoint (closure U₁) (closure U₂)
<VAR>A E : Type u<VAR>TopologicalSpace A<VAR>TopologicalSpace E<VAR>ExtremallyDisconnected A<VAR>T2Space A<VAR>T2Space E<VAR>CompactSpace E<VAR>ρ : E → A<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Function.Surjective ρ<VAR>zorn_subset : ∀ (E₀ : Set E), E₀ ≠ Set.univ → IsClosed E₀ → ρ '' E₀ ≠ Set.univ<GOAL>Function.Injective ρ
<VAR>A : Type u<VAR>TopologicalSpace A<VAR>ExtremallyDisconnected A<VAR>CompactSpace A<VAR>T2Space A<GOAL>CompactT2.Projective A
<VAR>A : Type u<VAR>TopologicalSpace A<VAR>CompactSpace A<VAR>T2Space A<GOAL>CompactT2.Projective A ↔ ExtremallyDisconnected A
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>x : tsze R M<GOAL>𝓝 x = (𝓝 x.fst).prod (𝓝 x.snd)
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>Zero M<VAR>x : R<GOAL>𝓝 (TrivSqZeroExt.inl x) = (𝓝 x).prod (𝓝 0)
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>Zero R<VAR>m : M<GOAL>𝓝 (TrivSqZeroExt.inr m) = (𝓝 0).prod (𝓝 m)
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<GOAL>Continuous TrivSqZeroExt.fst
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<GOAL>Continuous TrivSqZeroExt.snd
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>Zero M<GOAL>Continuous TrivSqZeroExt.inl
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>Zero R<GOAL>Continuous TrivSqZeroExt.inr
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>Zero M<GOAL>Embedding TrivSqZeroExt.inl
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>Zero R<GOAL>Embedding TrivSqZeroExt.inr
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : tsze R M<GOAL>(TrivSqZeroExt.fstCLM R M) x = x.fst
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : tsze R M<GOAL>(TrivSqZeroExt.sndCLM R M) x = x.snd
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>r : R<GOAL>(TrivSqZeroExt.inlCLM R M) r = TrivSqZeroExt.inl r
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<GOAL>(TrivSqZeroExt.inrCLM R M) m = TrivSqZeroExt.inr m
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>TopologicalSemiring R<VAR>ContinuousAdd M<VAR>ContinuousSMul R M<VAR>ContinuousSMul Rᵐᵒᵖ M<GOAL>TopologicalSemiring (tsze R M)
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>AddCommMonoid R<VAR>AddCommMonoid M<VAR>f : α → R<VAR>a : R<VAR>h : HasSum f a<GOAL>HasSum (fun x => TrivSqZeroExt.inl (f x)) (TrivSqZeroExt.inl a)
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>AddCommMonoid R<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a : M<VAR>h : HasSum f a<GOAL>HasSum (fun x => TrivSqZeroExt.inr (f x)) (TrivSqZeroExt.inr a)
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>AddCommMonoid R<VAR>AddCommMonoid M<VAR>f : α → tsze R M<VAR>a : tsze R M<VAR>h : HasSum f a<GOAL>HasSum (fun x => (f x).fst) a.fst
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>AddCommMonoid R<VAR>AddCommMonoid M<VAR>f : α → tsze R M<VAR>a : tsze R M<VAR>h : HasSum f a<GOAL>HasSum (fun x => (f x).snd) a.snd
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>UniformSpace R<VAR>UniformSpace M<GOAL>uniformity (tsze R M) = Filter.comap (fun p => (p.1.fst, p.2.fst)) (uniformity R) ⊓ Filter.comap (fun p => (p.1.snd, p.2.snd)) (uniformity M)
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>UniformSpace R<VAR>UniformSpace M<GOAL>UniformContinuous TrivSqZeroExt.fst
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>UniformSpace R<VAR>UniformSpace M<GOAL>UniformContinuous TrivSqZeroExt.snd
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>UniformSpace R<VAR>UniformSpace M<VAR>Zero M<GOAL>UniformContinuous TrivSqZeroExt.inl
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>UniformSpace R<VAR>UniformSpace M<VAR>Zero R<GOAL>UniformContinuous TrivSqZeroExt.inr
<VAR>K : Subfield ℂ<VAR>hc : IsClosed ↑K<GOAL>K = Complex.ofReal.fieldRange ∨ K = ⊤
<VAR>K : Subfield ℂ<VAR>ψ : ↥K →+* ℂ<VAR>hc : UniformContinuous ⇑ψ<GOAL>(↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>WeaklyLocallyCompactSpace X<VAR>K : Set X<VAR>hK : IsCompact K<GOAL>∃ K', IsCompact K' ∧ K ⊆ interior K'
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>WeaklyLocallyCompactSpace X<VAR>x : X<GOAL>Disjoint (𝓝 x) (Filter.cocompact X)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LocallyCompactSpace X<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsCompact s) fun s => s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LocallyCompactSpace X<VAR>x : X<VAR>n : Set X<VAR>h : n ∈ 𝓝 x<GOAL>∃ s ∈ 𝓝 x, s ⊆ n ∧ IsCompact s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : X → Type u_4<VAR>p : (x : X) → ι x → Prop<VAR>s : (x : X) → ι x → Set X<VAR>h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)<VAR>hc : ∀ (x : X) (i : ι x), p x i → IsCompact (s x i)<GOAL>LocallyCompactSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LocallyCompactSpace X<VAR>x : X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>hx : x ∈ U<GOAL>∃ K, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>LocallyCompactPair X Y<VAR>f : X → Y<VAR>K : Set X<VAR>U : Set Y<VAR>hf : Continuous f<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : Set.MapsTo f K U<GOAL>∃ L ∈ 𝓝ˢ K, IsCompact L ∧ Set.MapsTo f L U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LocallyCompactSpace X<VAR>K U : Set X<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>h_KU : K ⊆ U<GOAL>∃ L, IsCompact L ∧ K ⊆ interior L ∧ L ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>LocallyCompactSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>LocallyCompactSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LocallyCompactSpace X<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>LocallyCompactSpace ↑s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>LocallyCompactSpace Y<VAR>f : X → Y<VAR>hf : OpenEmbedding f<GOAL>LocallyCompactSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LocallyCompactSpace X<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>LocallyCompactSpace ↑s
<VAR>α : Type u_3<VAR>TopologicalSpace α<GOAL>QuasiSeparatedSpace α ↔ ∀ (U V : Set α), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>self : QuasiSeparatedSpace α<VAR>U V : Set α<GOAL>IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
<VAR>α : Type u_3<VAR>TopologicalSpace α<GOAL>IsQuasiSeparated Set.univ ↔ QuasiSeparatedSpace α
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>QuasiSeparatedSpace α<GOAL>IsQuasiSeparated Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>H : IsQuasiSeparated s<VAR>h : Embedding f<GOAL>IsQuasiSeparated (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>h : OpenEmbedding f<VAR>s : Set α<GOAL>IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>IsQuasiSeparated s ↔ QuasiSeparatedSpace ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>ht : IsQuasiSeparated t<VAR>h : s ⊆ t<GOAL>IsQuasiSeparated s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>QuasiSeparatedSpace α<GOAL>IsQuasiSeparated s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>h : OpenEmbedding f<VAR>QuasiSeparatedSpace β<GOAL>QuasiSeparatedSpace α
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsClopen s<GOAL>IsOpen s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsClopen s<GOAL>IsClosed s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsClopen s ↔ frontier s = ∅
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsClopen s<VAR>ht : IsClopen t<GOAL>IsClopen (s ∪ t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsClopen s<VAR>ht : IsClopen t<GOAL>IsClopen (s ∩ t)
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsClopen ∅
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsClopen Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsClopen s<GOAL>IsClopen sᶜ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsClopen sᶜ ↔ IsClopen s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsClopen s<VAR>ht : IsClopen t<GOAL>IsClopen (s \ t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsClopen s<VAR>ht : IsClopen t<GOAL>IsClopen (s ⇨ t)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<VAR>hs : IsClopen s<VAR>ht : IsClopen t<GOAL>IsClopen (s ×ˢ t)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>Finite Y<VAR>s : Y → Set X<VAR>h : ∀ (i : Y), IsClopen (s i)<GOAL>IsClopen (⋃ i, s i)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>s : Set Y<VAR>f : Y → Set X<VAR>hs : s.Finite<VAR>h : ∀ i ∈ s, IsClopen (f i)<GOAL>IsClopen (⋃ i ∈ s, f i)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>s : Finset Y<VAR>f : Y → Set X<VAR>h : ∀ i ∈ s, IsClopen (f i)<GOAL>IsClopen (⋃ i ∈ s, f i)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>Finite Y<VAR>s : Y → Set X<VAR>h : ∀ (i : Y), IsClopen (s i)<GOAL>IsClopen (⋂ i, s i)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>s : Set Y<VAR>hs : s.Finite<VAR>f : Y → Set X<VAR>h : ∀ i ∈ s, IsClopen (f i)<GOAL>IsClopen (⋂ i ∈ s, f i)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>s : Finset Y<VAR>f : Y → Set X<VAR>h : ∀ i ∈ s, IsClopen (f i)<GOAL>IsClopen (⋂ i ∈ s, f i)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set Y<VAR>h : IsClopen s<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>IsClopen (f ⁻¹' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>hf : ContinuousOn f s<VAR>hs : IsClopen s<VAR>ht : IsClopen t<GOAL>IsClopen (s ∩ f ⁻¹' t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s a b : Set X<VAR>h : IsClopen s<VAR>cover : s ⊆ a ∪ b<VAR>ha : IsOpen a<VAR>hb : IsOpen b<VAR>hab : Disjoint a b<GOAL>IsClopen (s ∩ a)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>DiscreteTopology X<VAR>s : Set X<GOAL>IsClopen s
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsClopen (Set.range Sum.inl)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>IsClopen (Set.range Sum.inr)
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (X i)<VAR>i : ι<GOAL>IsClopen (Set.range (Sigma.mk i))
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : QuotientMap f<VAR>s : Set Y<GOAL>IsClopen (f ⁻¹' s) ↔ IsClopen s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>U : Set X<GOAL>Continuous U.boolIndicator ↔ IsClopen U
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s U : Set X<GOAL>ContinuousOn U.boolIndicator s ↔ IsClopen (Subtype.val ⁻¹' U)