ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>b c : α<VAR>Add α<VAR>p : b = c<VAR>a : α<GOAL>a + b = a + c
<VAR>α : Type u_1<VAR>a₁ a₂ b₁ b₂ : α<VAR>Add α<VAR>p₁ : a₁ = b₁<VAR>p₂ : a₂ = b₂<GOAL>a₁ + a₂ = b₁ + b₂
<VAR>α : Type u_1<VAR>a b : α<VAR>Sub α<VAR>p : a = b<VAR>c : α<GOAL>a - c = b - c
<VAR>α : Type u_1<VAR>b c : α<VAR>Sub α<VAR>p : b = c<VAR>a : α<GOAL>a - b = a - c
<VAR>α : Type u_1<VAR>a₁ a₂ b₁ b₂ : α<VAR>Sub α<VAR>p₁ : a₁ = b₁<VAR>p₂ : a₂ = b₂<GOAL>a₁ - a₂ = b₁ - b₂
<VAR>α : Type u_1<VAR>a b : α<VAR>Neg α<VAR>p : a = b<GOAL>-a = -b
<VAR>α : Type u_1<VAR>a b : α<VAR>Mul α<VAR>p : a = b<VAR>c : α<GOAL>a * c = b * c
<VAR>α : Type u_1<VAR>b c : α<VAR>Mul α<VAR>p : b = c<VAR>a : α<GOAL>a * b = a * c
<VAR>α : Type u_1<VAR>a₁ a₂ b₁ b₂ : α<VAR>Mul α<VAR>p₁ : a₁ = b₁<VAR>p₂ : a₂ = b₂<GOAL>a₁ * a₂ = b₁ * b₂
<VAR>α : Type u_1<VAR>a b : α<VAR>Inv α<VAR>p : a = b<GOAL>a⁻¹ = b⁻¹
<VAR>α : Type u_1<VAR>a b : α<VAR>Div α<VAR>p : a = b<VAR>c : α<GOAL>a / c = b / c
<VAR>α : Type u_1<VAR>b c : α<VAR>Div α<VAR>p : b = c<VAR>a : α<GOAL>a / b = a / c
<VAR>α : Type u_1<VAR>a₁ a₂ b₁ b₂ : α<VAR>Div α<VAR>p₁ : a₁ = b₁<VAR>p₂ : a₂ = b₂<GOAL>a₁ / a₂ = b₁ / b₂
<VAR>α : Type u_1<VAR>a a' b b' : α<VAR>p : a = b<VAR>p₁ : a = a'<VAR>p₂ : b = b'<GOAL>a' = b'
<VAR>α : Type u_1<VAR>a a' b b' : α<VAR>AddGroup α<VAR>p : a = b<VAR>H : a' - b' - (a - b) = 0<GOAL>a' = b'
<VAR>α : Type u_1<VAR>a a' b b' : α<VAR>Ring α<VAR>NoZeroDivisors α<VAR>n : ℕ<VAR>p : a = b<VAR>H : (a' - b') ^ n - (a - b) = 0<GOAL>a' = b'
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>a b : α<VAR>ha : a = 0<VAR>hb : b = 0<GOAL>a + b = 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>a b : α<VAR>ha : a = 0<VAR>hb : b ≤ 0<GOAL>a + b ≤ 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>a b : α<VAR>ha : a = 0<VAR>hb : b < 0<GOAL>a + b < 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>a b : α<VAR>ha : a ≤ 0<VAR>hb : b = 0<GOAL>a + b ≤ 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b = 0<GOAL>a + b < 0
<VAR>α : Type u_1<VAR>StrictOrderedRing α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : 0 < b<GOAL>b * a < 0
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>a b : α<VAR>ha : a ≤ 0<VAR>hb : 0 < b<GOAL>b * a ≤ 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>a b : α<VAR>ha : a = 0<GOAL>0 < b → b * a = 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h1 : ¬a < b<VAR>h2 : ¬b < a<GOAL>a = b
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>Semiring α<VAR>a b : α<GOAL>R a 0 → b = 0 → a * b = 0
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>Semiring α<VAR>a b : α<VAR>h : a = 0<GOAL>R b 0 → a * b = 0
<VAR>α : Type u<VAR>OrderedSemiring α<VAR>n : ℕ<GOAL>0 ≤ ↑n
<VAR>α : Type u_1<VAR>Zero α<VAR>LT α<VAR>a : α<VAR>h : 0 > a<GOAL>a < 0
<VAR>α : Type u_1<VAR>Zero α<VAR>LE α<VAR>a : α<VAR>h : 0 ≥ a<GOAL>a ≤ 0
<VAR>α : Type u_1<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>LT α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < if p then a else b
<VAR>α : Type u_1<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>LE α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ if p then a else b
<VAR>α : Type u_1<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>Preorder α<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<GOAL>0 ≤ if p then a else b
<VAR>α : Type u_1<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>Preorder α<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<GOAL>0 ≤ if p then a else b
<VAR>α : Type u_1<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>(if p then a else b) ≠ 0
<VAR>α : Type u_1<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>Preorder α<VAR>ha : 0 < a<VAR>hb : b ≠ 0<GOAL>(if p then a else b) ≠ 0
<VAR>α : Type u_1<VAR>Zero α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>Preorder α<VAR>ha : a ≠ 0<VAR>hb : 0 < b<GOAL>(if p then a else b) ≠ 0
<VAR>R : Type u_2<VAR>LinearOrder R<VAR>a b c : R<VAR>ha : a < b<VAR>hb : a ≤ c<GOAL>a ≤ min b c
<VAR>R : Type u_2<VAR>LinearOrder R<VAR>a b c : R<VAR>ha : a ≤ b<VAR>hb : a < c<GOAL>a ≤ min b c
<VAR>R : Type u_2<VAR>LinearOrder R<VAR>a b c : R<VAR>ha : a ≠ c<VAR>hb : b ≠ c<GOAL>min a b ≠ c
<VAR>R : Type u_2<VAR>LinearOrder R<VAR>a b c : R<VAR>ha : a ≠ c<VAR>hb : c < b<GOAL>min a b ≠ c
<VAR>R : Type u_2<VAR>LinearOrder R<VAR>a b c : R<VAR>ha : c < a<VAR>hb : b ≠ c<GOAL>min a b ≠ c
<VAR>R : Type u_2<VAR>LinearOrder R<VAR>a b c : R<VAR>ha : a ≠ c<VAR>hb : b ≠ c<GOAL>max a b ≠ c
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a * b
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<GOAL>0 ≤ a * b
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>NoZeroDivisors α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : 0 < b<GOAL>a * b ≠ 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>NoZeroDivisors α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : b ≠ 0<GOAL>a * b ≠ 0
<VAR>a : ℤ<VAR>ha : 0 < a<GOAL>0 < a / a
<VAR>a b : ℤ<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a / b
<VAR>a b : ℤ<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<GOAL>0 ≤ a / b
<VAR>a b : ℤ<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 ≤ a / b
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>Nontrivial α<VAR>a : α<GOAL>0 < a ^ 0
<VAR>α : Type u_2<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a ≠ 0 → 0 < |a|
<VAR>n : ℤ<VAR>hn : 0 < n<GOAL>0 < n.natAbs
<VAR>R : Type u_1<VAR>Semiring R<VAR>a : R<GOAL>(Polynomial.C a).natDegree ≤ 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<GOAL>(↑n).natDegree ≤ 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Polynomial.natDegree 0 ≤ 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Polynomial.natDegree 1 ≤ 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>a b : R<VAR>f g : R[X]<VAR>h_add_left : f.coeff n = a<VAR>h_add_right : g.coeff n = b<GOAL>(f + g).coeff n = a + b
<VAR>R : Type u_1<VAR>Semiring R<VAR>d df dg : ℕ<VAR>a b : R<VAR>f g : R[X]<VAR>h_mul_left : f.natDegree ≤ df<VAR>h_mul_right : g.natDegree ≤ dg<GOAL>f.coeff df = a → g.coeff dg = b → df + dg ≤ d → (f * g).coeff d = if d = df + dg then a * b else 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>m n o : ℕ<VAR>a : R<VAR>p : R[X]<VAR>h_pow : p.natDegree ≤ n<VAR>h_exp : m * n ≤ o<VAR>h_pow_bas : p.coeff n = a<GOAL>(p ^ m).coeff o = if o = m * n then a ^ m else 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<VAR>f : R[X]<VAR>hf : f.natDegree ≤ n<GOAL>(a • f).natDegree ≤ n
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<VAR>f : R[X]<VAR>hf : f.degree ≤ ↑n<GOAL>(a • f).degree ≤ ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<VAR>f : R[X]<GOAL>(a • f).coeff n = a * f.coeff n
<VAR>R : Type u_1<VAR>Semiring R<VAR>deg m o : ℕ<VAR>c : R<VAR>p : R[X]<VAR>h_natDeg_le : p.natDegree ≤ m<VAR>coeff_eq : p.coeff o = c<VAR>coeff_ne_zero : c ≠ 0<VAR>deg_eq_deg : m = deg<VAR>coeff_eq_deg : o = deg<GOAL>p.natDegree = deg
<VAR>R : Type u_1<VAR>Semiring R<VAR>deg m o : WithBot ℕ<VAR>c : R<VAR>p : R[X]<VAR>h_deg_le : p.degree ≤ m<VAR>coeff_eq : p.coeff (WithBot.unbot' 0 deg) = c<VAR>coeff_ne_zero : c ≠ 0<VAR>deg_eq_deg : m = deg<VAR>coeff_eq_deg : o = deg<GOAL>p.degree = deg
<VAR>R : Type u_1<VAR>Semiring R<VAR>m n : ℕ<VAR>f : R[X]<VAR>r : R<VAR>h : f.coeff m = r<VAR>natDeg_eq_coeff : m = n<GOAL>f.coeff n = r
<VAR>R : Type u_1<VAR>Semiring R<VAR>m n : ℕ<VAR>f : R[X]<VAR>r : R<VAR>h : f.coeff m = r<VAR>natDeg_eq_coeff : m = n<VAR>s : R<VAR>rs : r = s<GOAL>f.coeff n = s
<VAR>R : Type u_1<VAR>Ring R<VAR>n : ℤ<GOAL>(↑n).natDegree ≤ 0
<VAR>R : Type u_1<VAR>Ring R<VAR>n : ℕ<VAR>a b : R<VAR>f g : R[X]<VAR>hf : f.coeff n = a<VAR>hg : g.coeff n = b<GOAL>(f - g).coeff n = a - b
<VAR>R : Type u_1<VAR>Ring R<VAR>n : ℕ<VAR>a : ℤ<GOAL>(↑a).coeff n = ↑(if n = 0 then a else 0)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>self : SeqCompactSpace X<GOAL>IsSeqCompact Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>SeqCompactSpace X ↔ IsSeqCompact Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>self : FrechetUrysohnSpace X<VAR>s : Set X<GOAL>closure s ⊆ seqClosure s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>self : SequentialSpace X<VAR>s : Set X<GOAL>IsSeqClosed s → IsClosed s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>SequentialSpace X<VAR>s : Set X<VAR>hs : IsSeqClosed s<GOAL>IsClosed s
<VAR>X : Type u<VAR>self : TopologicalSpace X<GOAL>TopologicalSpace.IsOpen Set.univ
<VAR>X : Type u<VAR>self : TopologicalSpace X<VAR>s : Set (Set X)<GOAL>(∀ (t : Set X), t ∈ s → TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
<VAR>X : Type u<VAR>self : TopologicalSpace X<VAR>s t : Set X<GOAL>TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsOpen Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsOpen s<VAR>ht : IsOpen t<GOAL>IsOpen (s ∩ t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set (Set X)<VAR>h : ∀ (t : Set X), t ∈ s → IsOpen t<GOAL>IsOpen (⋃₀ s)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>self : IsClosed s<GOAL>IsOpen sᶜ
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>self : Continuous f<VAR>s : Set Y<GOAL>IsOpen s → IsOpen (f ⁻¹' s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>self : BaireSpace X<VAR>f : ℕ → Set X<GOAL>(∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>a b : M<VAR>h : 1 * a = b<GOAL>a = b
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>self : α →CO β<GOAL>IsOpenMap self.toFun
<VAR>F : Type u_6<VAR>α : outParam (Type u_7)<VAR>β : outParam (Type u_8)<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>FunLike F α β<VAR>self : ContinuousOpenMapClass F α β<VAR>f : F<GOAL>IsOpenMap ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α →CO β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α →CO β<GOAL>⇑f.toContinuousMap = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f g : α →CO β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α →CO β<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 : α →CO β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>⇑(ContinuousOpenMap.id α) = id
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>a : α<GOAL>(ContinuousOpenMap.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : β →CO γ<VAR>g : α →CO β<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 : β →CO γ<VAR>g : α →CO β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<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 : γ →CO δ<VAR>g : β →CO γ<VAR>h : α →CO β<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 : α →CO β<GOAL>f.comp (ContinuousOpenMap.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α →CO β<GOAL>(ContinuousOpenMap.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₂ : β →CO γ<VAR>f : α →CO β<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 : β →CO γ<VAR>f₁ f₂ : α →CO β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u<VAR>Preorder α<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>x : α<GOAL>Scott.IsωSup c x ↔ IsLUB (Set.range ⇑c) x
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<GOAL>Scott.IsOpen α Set.univ
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>s t : Set α<GOAL>Scott.IsOpen α s → Scott.IsOpen α t → Scott.IsOpen α (s ∩ t)
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>s : Set (Set α)<VAR>hs : ∀ t ∈ s, Scott.IsOpen α t<GOAL>Scott.IsOpen α (⋃₀ s)
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>s : Set α<VAR>hs : Scott.IsOpen α s<GOAL>IsUpperSet s
<VAR>α : Type u_1<VAR>OmegaCompletePartialOrder α<VAR>y : Scott α<GOAL>IsOpen (notBelow y)
<VAR>α : Type u_1<VAR>OmegaCompletePartialOrder α<VAR>c : OmegaCompletePartialOrder.Chain α<GOAL>Scott.IsωSup c (OmegaCompletePartialOrder.ωSup c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>hf : Continuous f<GOAL>OmegaCompletePartialOrder.Continuous' f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>hf : OmegaCompletePartialOrder.Continuous' f<GOAL>Continuous f
<VAR>X : Type u_1<VAR>tX : TopologicalSpace X<VAR>S : Set (Set X)<VAR>self : RestrictGenTopology S<VAR>u : Set X<GOAL>(∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)) → IsOpen u
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>f : X → Y<VAR>self : Inducing f<GOAL>tX = TopologicalSpace.induced f tY
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>f : X → Y<GOAL>Inducing f ↔ tX = TopologicalSpace.induced f tY
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>Embedding f ↔ Inducing f ∧ Function.Injective f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>self : Embedding f<GOAL>Function.Injective f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>f : X → Y<VAR>self : OpenEmbedding f<GOAL>IsOpen (Set.range f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>f : X → Y<GOAL>OpenEmbedding f ↔ Embedding f ∧ IsOpen (Set.range f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>f : X → Y<VAR>self : ClosedEmbedding f<GOAL>IsClosed (Set.range f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>f : X → Y<GOAL>ClosedEmbedding f ↔ Embedding f ∧ IsClosed (Set.range f)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>Embedding (toPullbackDiag f)
<VAR>X₁ : Type u_1<VAR>X₂ : Type u_2<VAR>Y₁ : Sort u_3<VAR>Y₂ : Sort u_4<VAR>Z₁ : Type u_5<VAR>Z₂ : Type u_6<VAR>TopologicalSpace X₁<VAR>TopologicalSpace X₂<VAR>TopologicalSpace Z₁<VAR>TopologicalSpace Z₂<VAR>f₁ : X₁ → Y₁<VAR>g₁ : Z₁ → Y₁<VAR>f₂ : X₂ → Y₂<VAR>g₂ : Z₂ → Y₂<VAR>mapX : X₁ → X₂<VAR>contX : Continuous mapX<VAR>mapY : Y₁ → Y₂<VAR>mapZ : Z₁ → Z₂<VAR>contZ : Continuous mapZ<VAR>commX : f₂ ∘ mapX = mapY ∘ f₁<VAR>commZ : g₂ ∘ mapZ = mapY ∘ g₁<GOAL>Continuous (Function.mapPullback mapX mapY mapZ commX commZ)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>TopologicalSpace X<VAR>y : Y<GOAL>T2Space X ↔ IsSeparatedMap fun x => y
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>TopologicalSpace X<VAR>T2Space X<VAR>f : X → Y<GOAL>IsSeparatedMap f
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>inj : Function.Injective f<GOAL>IsSeparatedMap f
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>IsSeparatedMap f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → Disjoint (𝓝 x₁) (𝓝 x₂)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>IsSeparatedMap f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>IsSeparatedMap f ↔ IsClosed (Function.pullbackDiagonal f)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>IsSeparatedMap f ↔ ClosedEmbedding (toPullbackDiag f)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>IsSeparatedMap f ↔ IsClosedMap (toPullbackDiag f)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace A<VAR>f : X → Y<VAR>sep : IsSeparatedMap f<VAR>g : A → Y<GOAL>IsSeparatedMap Function.Pullback.snd
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type u_3<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>sep : IsSeparatedMap f<VAR>g : Y → A<VAR>inj : Function.Injective g<GOAL>IsSeparatedMap (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace A<VAR>f : X → Y<VAR>sep : IsSeparatedMap f<VAR>g : A → X<VAR>cont : Continuous g<VAR>inj : Function.Injective g<GOAL>IsSeparatedMap (f ∘ g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>inj : Function.Injective f<GOAL>IsLocallyInjective f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>IsLocallyInjective f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>IsLocallyInjective f ↔ IsOpen (Function.pullbackDiagonal f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>IsLocallyInjective f ↔ OpenEmbedding (toPullbackDiag f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : X → Y<GOAL>IsLocallyInjective f ↔ IsOpenMap (toPullbackDiag f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>y : Y<GOAL>DiscreteTopology X ↔ IsLocallyInjective fun x => y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type u_3<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>hf : IsLocallyInjective f<VAR>g : Y → A<VAR>hg : Function.Injective g<GOAL>IsLocallyInjective (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace A<VAR>f : X → Y<VAR>hf : IsLocallyInjective f<VAR>g : A → X<VAR>cont : Continuous g<VAR>hg : Function.Injective g<GOAL>IsLocallyInjective (f ∘ g)
<VAR>X : Type u_3<VAR>Y : Type u_2<VAR>A : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace A<VAR>f : X → Y<VAR>sep : IsSeparatedMap f<VAR>g₁ g₂ : A → X<VAR>h₁ : Continuous g₁<VAR>h₂ : Continuous g₂<VAR>he : f ∘ g₁ = f ∘ g₂<GOAL>IsClosed {a | g₁ a = g₂ a}
<VAR>X : Type u_3<VAR>Y : Type u_2<VAR>A : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace A<VAR>f : X → Y<VAR>inj : IsLocallyInjective f<VAR>g₁ g₂ : A → X<VAR>h₁ : Continuous g₁<VAR>h₂ : Continuous g₂<VAR>he : f ∘ g₁ = f ∘ g₂<GOAL>IsOpen {a | g₁ a = g₂ a}
<VAR>X : Type u_3<VAR>E : Type u_1<VAR>A : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace A<VAR>p : E → X<VAR>sep : IsSeparatedMap p<VAR>inj : IsLocallyInjective p<VAR>g₁ g₂ : A → E<VAR>PreconnectedSpace A<VAR>h₁ : Continuous g₁<VAR>h₂ : Continuous g₂<VAR>he : p ∘ g₁ = p ∘ g₂<VAR>a : A<VAR>ha : g₁ a = g₂ a<GOAL>g₁ = g₂
<VAR>X : Type u_3<VAR>E : Type u_1<VAR>A : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace A<VAR>p : E → X<VAR>sep : IsSeparatedMap p<VAR>inj : IsLocallyInjective p<VAR>s : Set A<VAR>hs : IsPreconnected s<VAR>g₁ g₂ : A → E<VAR>h₁ : ContinuousOn g₁ s<VAR>h₂ : ContinuousOn g₂ s<VAR>he : Set.EqOn (p ∘ g₁) (p ∘ g₂) s<VAR>a : A<VAR>has : a ∈ s<VAR>ha : g₁ a = g₂ a<GOAL>Set.EqOn g₁ g₂ s
<VAR>X : Type u_3<VAR>E : Type u_1<VAR>A : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace A<VAR>p : E → X<VAR>sep : IsSeparatedMap p<VAR>inj : IsLocallyInjective p<VAR>g : A → E<VAR>PreconnectedSpace A<VAR>cont : Continuous g<VAR>he : ∀ (a a' : A), p (g a) = p (g a')<VAR>a a' : A<GOAL>g a = g a'
<VAR>X : Type u_3<VAR>E : Type u_1<VAR>A : Type u_2<VAR>TopologicalSpace E<VAR>TopologicalSpace A<VAR>p : E → X<VAR>sep : IsSeparatedMap p<VAR>inj : IsLocallyInjective p<VAR>s : Set A<VAR>hs : IsPreconnected s<VAR>g : A → E<VAR>cont : ContinuousOn g s<VAR>he : ∀ a ∈ s, ∀ a' ∈ s, p (g a) = p (g a')<VAR>a a' : A<VAR>ha : a ∈ s<VAR>ha' : a' ∈ s<GOAL>g a = g a'
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>self : AlexandrovDiscrete α<VAR>S : Set (Set α)<GOAL>(∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S)
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>S : Set (Set α)<GOAL>(∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S)
<VAR>ι : Sort u_1<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>f : ι → Set α<VAR>hf : ∀ (i : ι), IsOpen (f i)<GOAL>IsOpen (⋂ i, f i)
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>f : (i : ι) → κ i → Set α<VAR>hf : ∀ (i : ι) (j : κ i), IsOpen (f i j)<GOAL>IsOpen (⋂ i, ⋂ j, f i j)
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>S : Set (Set α)<VAR>hS : ∀ s ∈ S, IsClosed s<GOAL>IsClosed (⋃₀ S)
<VAR>ι : Sort u_1<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>f : ι → Set α<VAR>hf : ∀ (i : ι), IsClosed (f i)<GOAL>IsClosed (⋃ i, f i)
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>f : (i : ι) → κ i → Set α<VAR>hf : ∀ (i : ι) (j : κ i), IsClosed (f i j)<GOAL>IsClosed (⋃ i, ⋃ j, f i j)
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>S : Set (Set α)<VAR>hS : ∀ s ∈ S, IsClopen s<GOAL>IsClopen (⋂₀ S)
<VAR>ι : Sort u_1<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>f : ι → Set α<VAR>hf : ∀ (i : ι), IsClopen (f i)<GOAL>IsClopen (⋂ i, f i)
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>f : (i : ι) → κ i → Set α<VAR>hf : ∀ (i : ι) (j : κ i), IsClopen (f i j)<GOAL>IsClopen (⋂ i, ⋂ j, f i j)
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>S : Set (Set α)<VAR>hS : ∀ s ∈ S, IsClopen s<GOAL>IsClopen (⋃₀ S)
<VAR>ι : Sort u_1<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>f : ι → Set α<VAR>hf : ∀ (i : ι), IsClopen (f i)<GOAL>IsClopen (⋃ i, f i)
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>f : (i : ι) → κ i → Set α<VAR>hf : ∀ (i : ι) (j : κ i), IsClopen (f i j)<GOAL>IsClopen (⋃ i, ⋃ j, f i j)
<VAR>ι : Sort u_1<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>f : ι → Set α<GOAL>interior (⋂ i, f i) = ⋂ i, interior (f i)
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>S : Set (Set α)<GOAL>interior (⋂₀ S) = ⋂ s ∈ S, interior s
<VAR>ι : Sort u_1<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>f : ι → Set α<GOAL>closure (⋃ i, f i) = ⋃ i, closure (f i)
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>S : Set (Set α)<GOAL>closure (⋃₀ S) = ⋃ s ∈ S, closure s
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>a : α<GOAL>exterior {a} = (𝓝 a).ker
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>exterior s = ⋂₀ {t | IsOpen t ∧ s ⊆ t}
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s : Set α<VAR>a : α<GOAL>a ∈ exterior s ↔ ∀ (U : Set α), IsOpen U → s ⊆ U → a ∈ U
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s t : Set α<GOAL>s ⊆ exterior t ↔ ∀ (U : Set α), IsOpen U → t ⊆ U → s ⊆ U
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>s ⊆ exterior s
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>h₁ : s ⊆ t<VAR>h₂ : IsOpen t<GOAL>exterior s ⊆ t
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s : Set α<VAR>h : IsOpen s<GOAL>exterior s = s
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>ht : IsOpen t<GOAL>exterior s ⊆ t ↔ s ⊆ t
<VAR>α : Type u_3<VAR>TopologicalSpace α<GOAL>Monotone exterior
<VAR>α : Type u_3<VAR>TopologicalSpace α<GOAL>exterior ∅ = ∅
<VAR>α : Type u_3<VAR>TopologicalSpace α<GOAL>exterior Set.univ = Set.univ
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>exterior s = ∅ ↔ s = ∅
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s : Set α<VAR>AlexandrovDiscrete α<GOAL>IsOpen (exterior s)
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s : Set α<VAR>AlexandrovDiscrete α<GOAL>exterior s ∈ 𝓝ˢ s
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s : Set α<VAR>AlexandrovDiscrete α<GOAL>exterior s = s ↔ IsOpen s
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s : Set α<VAR>AlexandrovDiscrete α<GOAL>exterior s ⊆ s ↔ IsOpen s
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>AlexandrovDiscrete α<GOAL>exterior s ⊆ t ↔ ∃ U, IsOpen U ∧ s ⊆ U ∧ U ⊆ t
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>AlexandrovDiscrete α<GOAL>exterior s ⊆ t ↔ t ∈ 𝓝ˢ s
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>t : Set α<VAR>a : α<VAR>AlexandrovDiscrete α<GOAL>exterior {a} ⊆ t ↔ t ∈ 𝓝 a