ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>M : Type u_10<VAR>α : Type u_11<VAR>TopologicalSpace X<VAR>Zero α<VAR>SMulZeroClass M α<VAR>f : X → M<VAR>g : X → α<GOAL>(tsupport fun x => f x • g x) ⊆ tsupport g
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace X<VAR>AddMonoid α<VAR>f g : X → α<GOAL>(tsupport fun x => f x + g x) ⊆ tsupport f ∪ tsupport g
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace X<VAR>Monoid α<VAR>f g : X → α<GOAL>(mulTSupport fun x => f x * g x) ⊆ mulTSupport f ∪ mulTSupport g
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>One β<VAR>f : α → β<VAR>x : α<GOAL>x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>Zero β<VAR>f : α → β<VAR>x : α<GOAL>x ∉ tsupport f ↔ f =ᶠ[𝓝 x] 0
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>Zero β<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : ∀ x ∈ tsupport f, ContinuousAt f x<GOAL>Continuous f
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>One β<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : ∀ x ∈ mulTSupport f, ContinuousAt f x<GOAL>Continuous f
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>Zero β<VAR>f : α → β<GOAL>HasCompactSupport f ↔ IsCompact (closure (Function.support f))
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>One β<VAR>f : α → β<GOAL>HasCompactMulSupport f ↔ IsCompact (closure (Function.mulSupport f))
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>One β<VAR>f : α → β<VAR>R1Space α<GOAL>(∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>Zero β<VAR>f : α → β<VAR>R1Space α<GOAL>(∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 0) ↔ HasCompactSupport f
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>One β<VAR>f : α → β<VAR>R1Space α<VAR>K : Set α<VAR>hK : IsCompact K<VAR>hfK : ∀ x ∉ K, f x = 1<GOAL>HasCompactMulSupport f
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>Zero β<VAR>f : α → β<VAR>R1Space α<VAR>K : Set α<VAR>hK : IsCompact K<VAR>hfK : ∀ x ∉ K, f x = 0<GOAL>HasCompactSupport f
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>One β<VAR>f : α → β<VAR>K : Set α<VAR>hK : IsCompact K<VAR>h'K : IsClosed K<VAR>hfK : ∀ x ∉ K, f x = 1<GOAL>HasCompactMulSupport f
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>Zero β<VAR>f : α → β<VAR>K : Set α<VAR>hK : IsCompact K<VAR>h'K : IsClosed K<VAR>hfK : ∀ x ∉ K, f x = 0<GOAL>HasCompactSupport f
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>Zero β<VAR>f : α → β<VAR>R1Space α<VAR>K : Set α<VAR>hK : IsCompact K<VAR>h : Function.support f ⊆ K<GOAL>HasCompactSupport f
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>One β<VAR>f : α → β<VAR>R1Space α<VAR>K : Set α<VAR>hK : IsCompact K<VAR>h : Function.mulSupport f ⊆ K<GOAL>HasCompactMulSupport f
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>Zero β<VAR>f : α → β<VAR>hf : HasCompactSupport f<GOAL>IsCompact (tsupport f)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>One β<VAR>f : α → β<VAR>hf : HasCompactMulSupport f<GOAL>IsCompact (mulTSupport f)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>One β<VAR>f : α → β<GOAL>HasCompactMulSupport f ↔ f =ᶠ[Filter.coclosedCompact α] 1
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>Zero β<VAR>f : α → β<GOAL>HasCompactSupport f ↔ f =ᶠ[Filter.coclosedCompact α] 0
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>Zero β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>hf : Continuous f<VAR>k : Set α<VAR>hk : IsCompact k<VAR>h'f : Function.support f ⊆ k<GOAL>IsCompact (Set.range f)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>One β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>hf : Continuous f<VAR>k : Set α<VAR>hk : IsCompact k<VAR>h'f : Function.mulSupport f ⊆ k<GOAL>IsCompact (Set.range f)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>One β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>h : HasCompactMulSupport f<VAR>hf : Continuous f<GOAL>IsCompact (Set.range f)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>Zero β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>h : HasCompactSupport f<VAR>hf : Continuous f<GOAL>IsCompact (Set.range f)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>TopologicalSpace α<VAR>Zero β<VAR>Zero γ<VAR>f : α → β<VAR>f' : α → γ<VAR>hf : HasCompactSupport f<VAR>hff' : Function.support f' ⊆ tsupport f<GOAL>HasCompactSupport f'
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>TopologicalSpace α<VAR>One β<VAR>One γ<VAR>f : α → β<VAR>f' : α → γ<VAR>hf : HasCompactMulSupport f<VAR>hff' : Function.mulSupport f' ⊆ mulTSupport f<GOAL>HasCompactMulSupport f'
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>TopologicalSpace α<VAR>Zero β<VAR>Zero γ<VAR>f : α → β<VAR>f' : α → γ<VAR>hf : HasCompactSupport f<VAR>hff' : Function.support f' ⊆ Function.support f<GOAL>HasCompactSupport f'
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>TopologicalSpace α<VAR>One β<VAR>One γ<VAR>f : α → β<VAR>f' : α → γ<VAR>hf : HasCompactMulSupport f<VAR>hff' : Function.mulSupport f' ⊆ Function.mulSupport f<GOAL>HasCompactMulSupport f'
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>TopologicalSpace α<VAR>Zero β<VAR>Zero γ<VAR>g : β → γ<VAR>f : α → β<VAR>hf : HasCompactSupport f<VAR>hg : g 0 = 0<GOAL>HasCompactSupport (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>TopologicalSpace α<VAR>One β<VAR>One γ<VAR>g : β → γ<VAR>f : α → β<VAR>hf : HasCompactMulSupport f<VAR>hg : g 1 = 1<GOAL>HasCompactMulSupport (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>TopologicalSpace α<VAR>Zero β<VAR>Zero γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : ∀ {x : β}, g x = 0 ↔ x = 0<GOAL>HasCompactSupport (g ∘ f) ↔ HasCompactSupport f
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>TopologicalSpace α<VAR>One β<VAR>One γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : ∀ {x : β}, g x = 1 ↔ x = 1<GOAL>HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f
<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace α'<VAR>One β<VAR>f : α → β<VAR>hf : HasCompactMulSupport f<VAR>g : α' → α<VAR>hg : ClosedEmbedding g<GOAL>HasCompactMulSupport (f ∘ g)
<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace α'<VAR>Zero β<VAR>f : α → β<VAR>hf : HasCompactSupport f<VAR>g : α' → α<VAR>hg : ClosedEmbedding g<GOAL>HasCompactSupport (f ∘ g)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>TopologicalSpace α<VAR>One β<VAR>One γ<VAR>One δ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>hf : HasCompactMulSupport f<VAR>hf₂ : HasCompactMulSupport f₂<VAR>hm : m 1 1 = 1<GOAL>HasCompactMulSupport fun x => m (f x) (f₂ x)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>TopologicalSpace α<VAR>Zero β<VAR>Zero γ<VAR>Zero δ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>hf : HasCompactSupport f<VAR>hf₂ : HasCompactSupport f₂<VAR>hm : m 0 0 = 0<GOAL>HasCompactSupport fun x => m (f x) (f₂ x)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>Zero β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>h'f : HasCompactSupport f<VAR>hf : Continuous f<VAR>k : Set β<VAR>hk : IsClosed k<VAR>h'k : 0 ∉ k<GOAL>IsCompact (f ⁻¹' k)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>One β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>h'f : HasCompactMulSupport f<VAR>hf : Continuous f<VAR>k : Set β<VAR>hk : IsClosed k<VAR>h'k : 1 ∉ k<GOAL>IsCompact (f ⁻¹' k)
<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace α'<VAR>One β<VAR>f : α → β<VAR>T2Space α'<VAR>hf : HasCompactMulSupport f<VAR>g : α → α'<VAR>cont : Continuous g<GOAL>mulTSupport (Function.extend g f 1) ⊆ g '' mulTSupport f
<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace α'<VAR>Zero β<VAR>f : α → β<VAR>T2Space α'<VAR>hf : HasCompactSupport f<VAR>g : α → α'<VAR>cont : Continuous g<GOAL>tsupport (Function.extend g f 0) ⊆ g '' tsupport f
<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace α'<VAR>Zero β<VAR>f : α → β<VAR>T2Space α'<VAR>hf : HasCompactSupport f<VAR>g : α → α'<VAR>cont : Continuous g<GOAL>HasCompactSupport (Function.extend g f 0)
<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace α'<VAR>One β<VAR>f : α → β<VAR>T2Space α'<VAR>hf : HasCompactMulSupport f<VAR>g : α → α'<VAR>cont : Continuous g<GOAL>HasCompactMulSupport (Function.extend g f 1)
<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace α'<VAR>One β<VAR>f : α → β<VAR>T2Space α'<VAR>hf : HasCompactMulSupport f<VAR>g : α → α'<VAR>cont : Continuous g<VAR>inj : Function.Injective g<GOAL>mulTSupport (Function.extend g f 1) = g '' mulTSupport f
<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace α'<VAR>Zero β<VAR>f : α → β<VAR>T2Space α'<VAR>hf : HasCompactSupport f<VAR>g : α → α'<VAR>cont : Continuous g<VAR>inj : Function.Injective g<GOAL>tsupport (Function.extend g f 0) = g '' tsupport f
<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>TopologicalSpace α'<VAR>Zero β<VAR>T2Space α'<VAR>TopologicalSpace β<VAR>U : Set α'<VAR>hU : IsOpen U<VAR>f : ↑U → β<VAR>cont : Continuous f<VAR>supp : HasCompactSupport f<GOAL>Continuous (Function.extend Subtype.val f 0)
<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>TopologicalSpace α'<VAR>One β<VAR>T2Space α'<VAR>TopologicalSpace β<VAR>U : Set α'<VAR>hU : IsOpen U<VAR>f : ↑U → β<VAR>cont : Continuous f<VAR>supp : HasCompactMulSupport f<GOAL>Continuous (Function.extend Subtype.val f 1)
<VAR>α : Type u_2<VAR>γ : Type u_5<VAR>TopologicalSpace α<VAR>f : α → γ<VAR>TopologicalSpace γ<VAR>One γ<VAR>h : HasCompactMulSupport f<GOAL>Filter.Tendsto f (Filter.cocompact α) (𝓝 1)
<VAR>α : Type u_2<VAR>γ : Type u_5<VAR>TopologicalSpace α<VAR>f : α → γ<VAR>TopologicalSpace γ<VAR>Zero γ<VAR>h : HasCompactSupport f<GOAL>Filter.Tendsto f (Filter.cocompact α) (𝓝 0)
<VAR>α : Type u_2<VAR>γ : Type u_5<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>Zero γ<VAR>f : α → γ<GOAL>HasCompactSupport f
<VAR>α : Type u_2<VAR>γ : Type u_5<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>One γ<VAR>f : α → γ<GOAL>HasCompactMulSupport f
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>AddZeroClass β<VAR>f f' : α → β<VAR>hf : HasCompactSupport f<VAR>hf' : HasCompactSupport f'<GOAL>HasCompactSupport (f + f')
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>MulOneClass β<VAR>f f' : α → β<VAR>hf : HasCompactMulSupport f<VAR>hf' : HasCompactMulSupport f'<GOAL>HasCompactMulSupport (f * f')
<VAR>α : Type u_2<VAR>M : Type u_7<VAR>R : Type u_9<VAR>TopologicalSpace α<VAR>Zero M<VAR>SMulZeroClass R M<VAR>f : α → R<VAR>f' : α → M<VAR>hf : HasCompactSupport f'<GOAL>HasCompactSupport (f • f')
<VAR>α : Type u_2<VAR>M : Type u_7<VAR>R : Type u_9<VAR>TopologicalSpace α<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>f : α → R<VAR>f' : α → M<VAR>hf : HasCompactSupport f<GOAL>HasCompactSupport (f • f')
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>MulZeroClass β<VAR>f f' : α → β<VAR>hf : HasCompactSupport f<GOAL>HasCompactSupport (f * f')
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>MulZeroClass β<VAR>f f' : α → β<VAR>hf : HasCompactSupport f'<GOAL>HasCompactSupport (f * f')
<VAR>α : Type u_10<VAR>β : Type u_11<VAR>TopologicalSpace α<VAR>AddGroup β<VAR>Lattice β<VAR>CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>f : α → β<VAR>hf : HasCompactSupport f<GOAL>HasCompactSupport |f|
<VAR>X : Type u_1<VAR>R : Type u_9<VAR>ι : Type u_10<VAR>TopologicalSpace X<VAR>U : ι → Set X<VAR>Zero R<VAR>f : ι → X → R<VAR>hlf : LocallyFinite fun i => Function.support (f i)<VAR>hso : ∀ (i : ι), tsupport (f i) ⊆ U i<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>x : X<GOAL>∃ is, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (Function.support fun i => f i z) ⊆ ↑is
<VAR>X : Type u_1<VAR>R : Type u_9<VAR>ι : Type u_10<VAR>TopologicalSpace X<VAR>U : ι → Set X<VAR>One R<VAR>f : ι → X → R<VAR>hlf : LocallyFinite fun i => Function.mulSupport (f i)<VAR>hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>x : X<GOAL>∃ is, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (Function.mulSupport fun i => f i z) ⊆ ↑is
<VAR>X : Type u_1<VAR>M : Type u_7<VAR>ι : Type u_10<VAR>TopologicalSpace X<VAR>AddCommMonoid M<VAR>f : ι → X → M<GOAL>(LocallyFinite fun i => Function.support (f i)) ↔ LocallyFinite fun i => tsupport (f i)
<VAR>X : Type u_1<VAR>M : Type u_7<VAR>ι : Type u_10<VAR>TopologicalSpace X<VAR>CommMonoid M<VAR>f : ι → X → M<GOAL>(LocallyFinite fun i => Function.mulSupport (f i)) ↔ LocallyFinite fun i => mulTSupport (f i)
<VAR>X : Type u_1<VAR>M : Type u_7<VAR>R : Type u_9<VAR>ι : Type u_10<VAR>TopologicalSpace X<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>s : ι → X → R<VAR>h : LocallyFinite fun i => Function.support (s i)<VAR>f : ι → X → M<GOAL>LocallyFinite fun i => Function.support (s i • f i)
<VAR>X : Type u_1<VAR>M : Type u_7<VAR>R : Type u_9<VAR>ι : Type u_10<VAR>TopologicalSpace X<VAR>Zero M<VAR>SMulZeroClass R M<VAR>f : ι → X → M<VAR>h : LocallyFinite fun i => Function.support (f i)<VAR>s : ι → X → R<GOAL>LocallyFinite fun i => Function.support (s i • f i)
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Preorder α<VAR>Preorder β<VAR>self : PseudoEpimorphism α β<VAR>a : α<VAR>b : β<GOAL>self.toFun a ≤ b → ∃ c, a ≤ c ∧ self.toFun c = b
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>self : EsakiaHom α β<VAR>a : α<VAR>b : β<GOAL>self.toFun a ≤ b → ∃ c, a ≤ c ∧ self.toFun c = b
<VAR>F : Type u_6<VAR>α : outParam (Type u_7)<VAR>β : outParam (Type u_8)<VAR>Preorder α<VAR>Preorder β<VAR>FunLike F α β<VAR>self : PseudoEpimorphismClass F α β<VAR>f : F<VAR>a : α<VAR>b : β<GOAL>f a ≤ b → ∃ c, a ≤ c ∧ f c = b
<VAR>F : Type u_6<VAR>α : outParam (Type u_7)<VAR>β : outParam (Type u_8)<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>FunLike F α β<VAR>self : EsakiaHomClass F α β<VAR>f : F<VAR>a : α<VAR>b : β<GOAL>f a ≤ b → ∃ c, a ≤ c ∧ f c = b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : PseudoEpimorphism α β<GOAL>⇑f.toOrderHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : PseudoEpimorphism α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f g : PseudoEpimorphism α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : PseudoEpimorphism α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : PseudoEpimorphism α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>Preorder α<GOAL>⇑(PseudoEpimorphism.id α) = id
<VAR>α : Type u_2<VAR>Preorder α<GOAL>↑(PseudoEpimorphism.id α) = OrderHom.id
<VAR>α : Type u_2<VAR>Preorder α<VAR>a : α<GOAL>(PseudoEpimorphism.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : PseudoEpimorphism β γ<VAR>f : PseudoEpimorphism α β<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : PseudoEpimorphism β γ<VAR>f : PseudoEpimorphism α β<GOAL>↑(g.comp f) = (↑g).comp ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : PseudoEpimorphism β γ<VAR>f : PseudoEpimorphism α β<VAR>a : α<GOAL>(g.comp f) a = g (f a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>Preorder δ<VAR>h : PseudoEpimorphism γ δ<VAR>g : PseudoEpimorphism β γ<VAR>f : PseudoEpimorphism α β<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : PseudoEpimorphism α β<GOAL>f.comp (PseudoEpimorphism.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : PseudoEpimorphism α β<GOAL>(PseudoEpimorphism.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g₁ g₂ : PseudoEpimorphism β γ<VAR>f : PseudoEpimorphism α β<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>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : PseudoEpimorphism β γ<VAR>f₁ f₂ : PseudoEpimorphism α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f : EsakiaHom α β<GOAL>⇑f.toContinuousOrderHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f : EsakiaHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f g : EsakiaHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f : EsakiaHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f : EsakiaHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<GOAL>⇑(EsakiaHom.id α) = id
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<GOAL>{ toOrderHom := ↑(EsakiaHom.id α), exists_map_eq_of_map_le' := ⋯ } = PseudoEpimorphism.id α
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<VAR>a : α<GOAL>(EsakiaHom.id α) a = a
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<GOAL>↑(EsakiaHom.id α) = ContinuousOrderHom.id α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>TopologicalSpace γ<VAR>Preorder γ<VAR>g : EsakiaHom β γ<VAR>f : EsakiaHom α β<GOAL>↑(g.comp f) = (↑g).comp ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>TopologicalSpace γ<VAR>Preorder γ<VAR>g : EsakiaHom β γ<VAR>f : EsakiaHom α β<GOAL>{ toOrderHom := ↑(g.comp f), exists_map_eq_of_map_le' := ⋯ } = { toOrderHom := ↑g, exists_map_eq_of_map_le' := ⋯ }.comp { toOrderHom := ↑f, exists_map_eq_of_map_le' := ⋯ }
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>TopologicalSpace γ<VAR>Preorder γ<VAR>g : EsakiaHom β γ<VAR>f : EsakiaHom α β<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>TopologicalSpace γ<VAR>Preorder γ<VAR>g : EsakiaHom β γ<VAR>f : EsakiaHom α β<VAR>a : α<GOAL>(g.comp f) a = g (f a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>TopologicalSpace γ<VAR>Preorder γ<VAR>TopologicalSpace δ<VAR>Preorder δ<VAR>h : EsakiaHom γ δ<VAR>g : EsakiaHom β γ<VAR>f : EsakiaHom α β<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f : EsakiaHom α β<GOAL>f.comp (EsakiaHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f : EsakiaHom α β<GOAL>(EsakiaHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>TopologicalSpace γ<VAR>Preorder γ<VAR>g₁ g₂ : EsakiaHom β γ<VAR>f : EsakiaHom α β<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>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>TopologicalSpace γ<VAR>Preorder γ<VAR>g : EsakiaHom β γ<VAR>f₁ f₂ : EsakiaHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>L : Type u_1<VAR>SemilatticeSup L<VAR>TopologicalSpace L<VAR>ContinuousSup L<VAR>α : Type u_2<VAR>l : Filter α<VAR>f : ℕ → α → L<VAR>g : ℕ → L<VAR>n : ℕ<VAR>hf : ∀ k ≤ n, Filter.Tendsto (f k) l (𝓝 (g k))<GOAL>Filter.Tendsto ((partialSups f) n) l (𝓝 ((partialSups g) n))
<VAR>L : Type u_1<VAR>SemilatticeSup L<VAR>TopologicalSpace L<VAR>ContinuousSup L<VAR>α : Type u_2<VAR>l : Filter α<VAR>f : ℕ → α → L<VAR>g : ℕ → L<VAR>n : ℕ<VAR>hf : ∀ k ≤ n, Filter.Tendsto (f k) l (𝓝 (g k))<GOAL>Filter.Tendsto (fun a => (partialSups fun x => f x a) n) l (𝓝 ((partialSups g) n))
<VAR>L : Type u_1<VAR>SemilatticeSup L<VAR>TopologicalSpace L<VAR>ContinuousSup L<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>f : ℕ → X → L<VAR>n : ℕ<VAR>x : X<VAR>hf : ∀ k ≤ n, ContinuousAt (f k) x<GOAL>ContinuousAt (fun a => (partialSups fun x => f x a) n) x
<VAR>L : Type u_1<VAR>SemilatticeSup L<VAR>TopologicalSpace L<VAR>ContinuousSup L<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>f : ℕ → X → L<VAR>n : ℕ<VAR>x : X<VAR>hf : ∀ k ≤ n, ContinuousAt (f k) x<GOAL>ContinuousAt ((partialSups f) n) x
<VAR>L : Type u_1<VAR>SemilatticeSup L<VAR>TopologicalSpace L<VAR>ContinuousSup L<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>f : ℕ → X → L<VAR>n : ℕ<VAR>s : Set X<VAR>x : X<VAR>hf : ∀ k ≤ n, ContinuousWithinAt (f k) s x<GOAL>ContinuousWithinAt (fun a => (partialSups fun x => f x a) n) s x
<VAR>L : Type u_1<VAR>SemilatticeSup L<VAR>TopologicalSpace L<VAR>ContinuousSup L<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>f : ℕ → X → L<VAR>n : ℕ<VAR>s : Set X<VAR>x : X<VAR>hf : ∀ k ≤ n, ContinuousWithinAt (f k) s x<GOAL>ContinuousWithinAt ((partialSups f) n) s x
<VAR>L : Type u_1<VAR>SemilatticeSup L<VAR>TopologicalSpace L<VAR>ContinuousSup L<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>f : ℕ → X → L<VAR>n : ℕ<VAR>s : Set X<VAR>hf : ∀ k ≤ n, ContinuousOn (f k) s<GOAL>ContinuousOn (fun a => (partialSups fun x => f x a) n) s
<VAR>L : Type u_1<VAR>SemilatticeSup L<VAR>TopologicalSpace L<VAR>ContinuousSup L<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>f : ℕ → X → L<VAR>n : ℕ<VAR>s : Set X<VAR>hf : ∀ k ≤ n, ContinuousOn (f k) s<GOAL>ContinuousOn ((partialSups f) n) s
<VAR>L : Type u_1<VAR>SemilatticeSup L<VAR>TopologicalSpace L<VAR>ContinuousSup L<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>f : ℕ → X → L<VAR>n : ℕ<VAR>hf : ∀ k ≤ n, Continuous (f k)<GOAL>Continuous fun a => (partialSups fun x => f x a) n
<VAR>L : Type u_1<VAR>SemilatticeSup L<VAR>TopologicalSpace L<VAR>ContinuousSup L<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>f : ℕ → X → L<VAR>n : ℕ<VAR>hf : ∀ k ≤ n, Continuous (f k)<GOAL>Continuous ((partialSups f) n)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>self : TopologicalSpace.NoetherianSpace α<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>TopologicalSpace.NoetherianSpace α ↔ WellFounded fun x x_1 => x > x_1
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>TopologicalSpace.NoetherianSpace α ↔ ∀ (s : TopologicalSpace.Opens α), IsCompact ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>TopologicalSpace.NoetherianSpace α<VAR>s : Set α<GOAL>IsCompact s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.NoetherianSpace α<VAR>i : β → α<VAR>hi : Inducing i<GOAL>TopologicalSpace.NoetherianSpace β
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>[TopologicalSpace.NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : TopologicalSpace.Opens α), IsCompact ↑s].TFAE
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>TopologicalSpace.NoetherianSpace α ↔ ∀ (s : Set α), IsCompact s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>TopologicalSpace.NoetherianSpace α<GOAL>WellFounded fun s t => s < t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.NoetherianSpace α<VAR>f : α → β<VAR>hf : Continuous f<VAR>hf' : Function.Surjective f<GOAL>TopologicalSpace.NoetherianSpace β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α ≃ₜ β<GOAL>TopologicalSpace.NoetherianSpace α ↔ TopologicalSpace.NoetherianSpace β