ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>a : X<VAR>l : Filter X<VAR>ha : a ∈ s<VAR>l.NeBot<VAR>hl : l ≤ 𝓟 s<VAR>f g : X → α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<VAR>ha' : f a ≤ g a<VAR>he : g ≤ᶠ[l] f<GOAL>∃ x ∈ s, f x = g x
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>l₁ l₂ : Filter X<VAR>l₁.NeBot<VAR>l₂.NeBot<VAR>hl₁ : l₁ ≤ 𝓟 s<VAR>hl₂ : l₂ ≤ 𝓟 s<VAR>f g : X → α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<VAR>he₁ : f ≤ᶠ[l₁] g<VAR>he₂ : g ≤ᶠ[l₂] f<GOAL>∃ x ∈ s, f x = g x
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>a b : X<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>f : X → α<VAR>hf : ContinuousOn f s<GOAL>Set.Icc (f a) (f b) ⊆ f '' s
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>a : X<VAR>l : Filter X<VAR>ha : a ∈ s<VAR>l.NeBot<VAR>hl : l ≤ 𝓟 s<VAR>f : X → α<VAR>hf : ContinuousOn f s<VAR>v : α<VAR>ht : Filter.Tendsto f l (𝓝 v)<GOAL>Set.Ico (f a) v ⊆ f '' s
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>a : X<VAR>l : Filter X<VAR>ha : a ∈ s<VAR>l.NeBot<VAR>hl : l ≤ 𝓟 s<VAR>f : X → α<VAR>hf : ContinuousOn f s<VAR>v : α<VAR>ht : Filter.Tendsto f l (𝓝 v)<GOAL>Set.Ioc v (f a) ⊆ f '' s
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>l₁ l₂ : Filter X<VAR>l₁.NeBot<VAR>l₂.NeBot<VAR>hl₁ : l₁ ≤ 𝓟 s<VAR>hl₂ : l₂ ≤ 𝓟 s<VAR>f : X → α<VAR>hf : ContinuousOn f s<VAR>v₁ v₂ : α<VAR>ht₁ : Filter.Tendsto f l₁ (𝓝 v₁)<VAR>ht₂ : Filter.Tendsto f l₂ (𝓝 v₂)<GOAL>Set.Ioo v₁ v₂ ⊆ f '' s
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>a : X<VAR>l : Filter X<VAR>ha : a ∈ s<VAR>l.NeBot<VAR>hl : l ≤ 𝓟 s<VAR>f : X → α<VAR>hf : ContinuousOn f s<VAR>ht : Filter.Tendsto f l Filter.atTop<GOAL>Set.Ici (f a) ⊆ f '' s
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>a : X<VAR>l : Filter X<VAR>ha : a ∈ s<VAR>l.NeBot<VAR>hl : l ≤ 𝓟 s<VAR>f : X → α<VAR>hf : ContinuousOn f s<VAR>ht : Filter.Tendsto f l Filter.atBot<GOAL>Set.Iic (f a) ⊆ f '' s
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>l₁ l₂ : Filter X<VAR>l₁.NeBot<VAR>l₂.NeBot<VAR>hl₁ : l₁ ≤ 𝓟 s<VAR>hl₂ : l₂ ≤ 𝓟 s<VAR>f : X → α<VAR>hf : ContinuousOn f s<VAR>v : α<VAR>ht₁ : Filter.Tendsto f l₁ (𝓝 v)<VAR>ht₂ : Filter.Tendsto f l₂ Filter.atTop<GOAL>Set.Ioi v ⊆ f '' s
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>l₁ l₂ : Filter X<VAR>l₁.NeBot<VAR>l₂.NeBot<VAR>hl₁ : l₁ ≤ 𝓟 s<VAR>hl₂ : l₂ ≤ 𝓟 s<VAR>f : X → α<VAR>hf : ContinuousOn f s<VAR>v : α<VAR>ht₁ : Filter.Tendsto f l₁ Filter.atBot<VAR>ht₂ : Filter.Tendsto f l₂ (𝓝 v)<GOAL>Set.Iio v ⊆ f '' s
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>l₁ l₂ : Filter X<VAR>l₁.NeBot<VAR>l₂.NeBot<VAR>hl₁ : l₁ ≤ 𝓟 s<VAR>hl₂ : l₂ ≤ 𝓟 s<VAR>f : X → α<VAR>hf : ContinuousOn f s<VAR>ht₁ : Filter.Tendsto f l₁ Filter.atBot<VAR>ht₂ : Filter.Tendsto f l₂ Filter.atTop<GOAL>Set.univ ⊆ f '' s
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>PreconnectedSpace X<VAR>a b : X<VAR>f : X → α<VAR>hf : Continuous f<GOAL>Set.Icc (f a) (f b) ⊆ Set.range f
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>PreconnectedSpace X<VAR>c : α<VAR>f : X → α<VAR>hf : Continuous f<VAR>h₁ : ∃ a, f a ≤ c<VAR>h₂ : ∃ b, c ≤ f b<GOAL>c ∈ Set.range f
<VAR>α : Type v<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set α<VAR>hs : IsPreconnected s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>Set.Icc a b ⊆ s
<VAR>α : Type v<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set α<VAR>h : IsPreconnected s<GOAL>s.OrdConnected
<VAR>α : Type v<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set α<VAR>hs : IsConnected s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>Set.Icc a b ⊆ s
<VAR>α : Type v<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set α<VAR>hs : IsPreconnected s<VAR>hb : ¬BddBelow s<VAR>ha : ¬BddAbove s<GOAL>s = Set.univ
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hs : IsConnected s<VAR>hb : BddBelow s<VAR>ha : BddAbove s<GOAL>Set.Ioo (sInf s) (sSup s) ⊆ s
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hc : IsConnected s<VAR>hb : BddBelow s<VAR>ha : BddAbove s<VAR>hcl : IsClosed s<GOAL>s = Set.Icc (sInf s) (sSup s)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hs : IsPreconnected s<VAR>hb : BddBelow s<VAR>ha : ¬BddAbove s<GOAL>Set.Ioi (sInf s) ⊆ s
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hs : IsPreconnected s<VAR>hb : ¬BddBelow s<VAR>ha : BddAbove s<GOAL>Set.Iio (sSup s) ⊆ s
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hs : IsPreconnected s<GOAL>s ∈ {Set.Icc (sInf s) (sSup s), Set.Ico (sInf s) (sSup s), Set.Ioc (sInf s) (sSup s), Set.Ioo (sInf s) (sSup s), Set.Ici (sInf s), Set.Ioi (sInf s), Set.Iic (sSup s), Set.Iio (sSup s), Set.univ, ∅}
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<GOAL>{s | IsPreconnected s} ⊆ Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪ Set.range (Function.uncurry Set.Ioc) ∪ Set.range (Function.uncurry Set.Ioo) ∪ (Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Set.Icc a b)<VAR>ha : a ∈ s<VAR>hab : a ≤ b<VAR>hgt : ∀ x ∈ s ∩ Set.Ico a b, (s ∩ Set.Ioc x b).Nonempty<GOAL>b ∈ s
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Set.Icc a b)<VAR>ha : a ∈ s<VAR>hgt : ∀ x ∈ s ∩ Set.Ico a b, ∀ y ∈ Set.Ioi x, (s ∩ Set.Ioc x y).Nonempty<GOAL>Set.Icc a b ⊆ s
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Set.Icc a b)<VAR>ha : a ∈ s<VAR>hgt : ∀ x ∈ s ∩ Set.Ico a b, s ∈ 𝓝[>] x<GOAL>Set.Icc a b ⊆ s
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>x y : α<VAR>s t : Set α<VAR>hxy : x ≤ y<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Set.Icc a b ⊆ s ∪ t<VAR>hx : x ∈ Set.Icc a b ∩ s<VAR>hy : y ∈ Set.Icc a b ∩ t<GOAL>(Set.Icc a b ∩ (s ∩ t)).Nonempty
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<GOAL>IsPreconnected (Set.Icc a b)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<GOAL>IsPreconnected (Set.uIcc a b)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>s : Set α<VAR>h : s.OrdConnected<GOAL>IsPreconnected s
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>s : Set α<GOAL>IsPreconnected s ↔ s.OrdConnected
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<GOAL>IsPreconnected (Set.Ici a)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<GOAL>IsPreconnected (Set.Iic a)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<GOAL>IsPreconnected (Set.Iio a)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<GOAL>IsPreconnected (Set.Ioi a)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<GOAL>IsPreconnected (Set.Ioo a b)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<GOAL>IsPreconnected (Set.Ioc a b)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<GOAL>IsPreconnected (Set.Ico a b)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<GOAL>IsConnected (Set.Ici a)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<GOAL>IsConnected (Set.Iic a)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>NoMaxOrder α<GOAL>IsConnected (Set.Ioi a)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>NoMinOrder α<GOAL>IsConnected (Set.Iio a)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a ≤ b<GOAL>IsConnected (Set.Icc a b)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>IsConnected (Set.Ioo a b)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>IsConnected (Set.Ioc a b)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>IsConnected (Set.Ico a b)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<GOAL>{s | IsPreconnected s} = Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪ Set.range (Function.uncurry Set.Ioc) ∪ Set.range (Function.uncurry Set.Ioo) ∪ (Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>s : Set α<GOAL>IsTotallyDisconnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Set.Ioo x y
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>a b : α<VAR>hab : a ≤ b<VAR>f : α → δ<VAR>hf : ContinuousOn f (Set.Icc a b)<GOAL>Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>a b : α<VAR>hab : a ≤ b<VAR>f : α → δ<VAR>hf : ContinuousOn f (Set.Icc a b)<GOAL>Set.Icc (f b) (f a) ⊆ f '' Set.Icc a b
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>a b : α<VAR>f : α → δ<VAR>hf : ContinuousOn f (Set.uIcc a b)<GOAL>Set.uIcc (f a) (f b) ⊆ f '' Set.uIcc a b
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>a b : α<VAR>hab : a ≤ b<VAR>f : α → δ<VAR>hf : ContinuousOn f (Set.Icc a b)<GOAL>Set.Ico (f a) (f b) ⊆ f '' Set.Ico a b
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>a b : α<VAR>hab : a ≤ b<VAR>f : α → δ<VAR>hf : ContinuousOn f (Set.Icc a b)<GOAL>Set.Ioc (f b) (f a) ⊆ f '' Set.Ico a b
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>a b : α<VAR>hab : a ≤ b<VAR>f : α → δ<VAR>hf : ContinuousOn f (Set.Icc a b)<GOAL>Set.Ioc (f a) (f b) ⊆ f '' Set.Ioc a b
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>a b : α<VAR>hab : a ≤ b<VAR>f : α → δ<VAR>hf : ContinuousOn f (Set.Icc a b)<GOAL>Set.Ico (f b) (f a) ⊆ f '' Set.Ioc a b
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>a b : α<VAR>hab : a ≤ b<VAR>f : α → δ<VAR>hf : ContinuousOn f (Set.Icc a b)<GOAL>Set.Ioo (f a) (f b) ⊆ f '' Set.Ioo a b
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>a b : α<VAR>hab : a ≤ b<VAR>f : α → δ<VAR>hf : ContinuousOn f (Set.Icc a b)<GOAL>Set.Ioo (f b) (f a) ⊆ f '' Set.Ioo a b
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>s : Set α<VAR>hs : s.OrdConnected<VAR>f : α → δ<VAR>hf : ContinuousOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>Set.SurjOn f s (Set.Icc (f a) (f b))
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>s : Set α<VAR>hs : s.OrdConnected<VAR>f : α → δ<VAR>hf : ContinuousOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>Set.SurjOn f s (Set.uIcc (f a) (f b))
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>f : α → δ<VAR>hf : Continuous f<VAR>h_top : Filter.Tendsto f Filter.atTop Filter.atTop<VAR>h_bot : Filter.Tendsto f Filter.atBot Filter.atBot<GOAL>Function.Surjective f
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>f : α → δ<VAR>hf : Continuous f<VAR>h_top : Filter.Tendsto f Filter.atBot Filter.atTop<VAR>h_bot : Filter.Tendsto f Filter.atTop Filter.atBot<GOAL>Function.Surjective f
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>f : α → δ<VAR>s : Set α<VAR>s.OrdConnected<VAR>hs : s.Nonempty<VAR>hf : ContinuousOn f s<VAR>hbot : Filter.Tendsto (fun x => f ↑x) Filter.atBot Filter.atBot<VAR>htop : Filter.Tendsto (fun x => f ↑x) Filter.atTop Filter.atTop<GOAL>Set.SurjOn f s Set.univ
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>f : α → δ<VAR>s : Set α<VAR>s.OrdConnected<VAR>hs : s.Nonempty<VAR>hf : ContinuousOn f s<VAR>hbot : Filter.Tendsto (fun x => f ↑x) Filter.atBot Filter.atTop<VAR>htop : Filter.Tendsto (fun x => f ↑x) Filter.atTop Filter.atBot<GOAL>Set.SurjOn f s Set.univ
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>BoundedOrder α<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf : f ⊥ ≤ f ⊤<VAR>hf_i : Function.Injective f<GOAL>StrictMono f
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>BoundedOrder α<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf : f ⊤ ≤ f ⊥<VAR>hf_i : Function.Injective f<GOAL>StrictAnti f
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>BoundedOrder α<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Function.Injective f<GOAL>StrictMono f ∨ StrictAnti f
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Function.Injective f<VAR>a b : α<VAR>hab : a < b<VAR>hf_mono : StrictMonoOn f (Set.Icc a b)<GOAL>StrictMono f
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>a b : α<VAR>f : α → δ<VAR>hab : a ≤ b<VAR>hfab : f a ≤ f b<VAR>hf_c : ContinuousOn f (Set.Icc a b)<VAR>hf_i : Set.InjOn f (Set.Icc a b)<GOAL>StrictMonoOn f (Set.Icc a b)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>a b : α<VAR>f : α → δ<VAR>hab : a ≤ b<VAR>hfab : f b ≤ f a<VAR>hf_c : ContinuousOn f (Set.Icc a b)<VAR>hf_i : Set.InjOn f (Set.Icc a b)<GOAL>StrictAntiOn f (Set.Icc a b)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>a b : α<VAR>f : α → δ<VAR>hab : a ≤ b<VAR>hf_c : ContinuousOn f (Set.Icc a b)<VAR>hf_i : Set.InjOn f (Set.Icc a b)<GOAL>StrictMonoOn f (Set.Icc a b) ∨ StrictAntiOn f (Set.Icc a b)
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Function.Injective f<GOAL>StrictMono f ∨ StrictAnti f
<VAR>α : Type u<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>δ : Type u_1<VAR>LinearOrder δ<VAR>TopologicalSpace δ<VAR>OrderClosedTopology δ<VAR>a b : α<VAR>f : α → δ<VAR>hab : a < b<VAR>hf_c : ContinuousOn f (Set.Ioo a b)<VAR>hf_i : Set.InjOn f (Set.Ioo a b)<GOAL>StrictMonoOn f (Set.Ioo a b) ∨ StrictAntiOn f (Set.Ioo a b)
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>F : Type u_2<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>TopologicalSpace F<VAR>ContinuousSMul ℝ F<VAR>T2Space F<VAR>G : Type u_3<VAR>FunLike G E F<VAR>AddMonoidHomClass G E F<VAR>f : G<VAR>hf : Continuous ⇑f<VAR>c : ℝ<VAR>x : E<GOAL>f (c • x) = c • f x
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>F : Type u_2<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>TopologicalSpace F<VAR>ContinuousSMul ℝ F<VAR>T2Space F<VAR>f : E →+ F<VAR>hf : Continuous ⇑f<GOAL>⇑(f.toRealLinearMap hf) = ⇑f
<VAR>α : Type u_2<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_8<VAR>TopologicalSpace R<VAR>TopologicalSpace α<VAR>f : α → Matrix m n R<VAR>h : ∀ (i : m) (j : n), Continuous fun a => f a i j<GOAL>Continuous f
<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>A : X → Matrix m n R<VAR>hA : Continuous A<VAR>i : m<VAR>j : n<GOAL>Continuous fun x => A x i j
<VAR>X : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>S : Type u_7<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>TopologicalSpace S<VAR>A : X → Matrix m n S<VAR>f : S → R<VAR>hA : Continuous A<VAR>hf : Continuous f<GOAL>Continuous fun x => (A x).map f
<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>A : X → Matrix m n R<VAR>hA : Continuous A<GOAL>Continuous fun x => (A 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>Star R<VAR>ContinuousStar R<VAR>A : X → Matrix m n R<VAR>hA : Continuous A<GOAL>Continuous fun x => (A x)ᴴ
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>ι : Type u_11<VAR>A : X → n → R<VAR>hA : Continuous A<GOAL>Continuous fun x => Matrix.col ι (A x)
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>ι : Type u_11<VAR>A : X → n → R<VAR>hA : Continuous A<GOAL>Continuous fun x => Matrix.row ι (A x)
<VAR>X : Type u_1<VAR>n : Type u_5<VAR>R : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>Zero R<VAR>DecidableEq n<VAR>A : X → n → R<VAR>hA : Continuous A<GOAL>Continuous fun x => Matrix.diagonal (A 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>Mul R<VAR>AddCommMonoid R<VAR>ContinuousAdd R<VAR>ContinuousMul R<VAR>A B : X → n → R<VAR>hA : Continuous A<VAR>hB : Continuous B<GOAL>Continuous fun x => A x ⬝ᵥ B 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>Fintype n<VAR>Mul R<VAR>AddCommMonoid R<VAR>ContinuousAdd R<VAR>ContinuousMul R<VAR>A : X → Matrix m n R<VAR>B : X → Matrix n p R<VAR>hA : Continuous A<VAR>hB : Continuous B<GOAL>Continuous fun x => A x * 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>Mul R<VAR>ContinuousMul R<VAR>A : X → m → R<VAR>B : X → n → R<VAR>hA : Continuous A<VAR>hB : Continuous B<GOAL>Continuous fun x => Matrix.vecMulVec (A x) (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>NonUnitalNonAssocSemiring R<VAR>ContinuousAdd R<VAR>ContinuousMul R<VAR>Fintype n<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 *ᵥ 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>NonUnitalNonAssocSemiring R<VAR>ContinuousAdd R<VAR>ContinuousMul R<VAR>Fintype m<VAR>A : X → m → R<VAR>B : X → Matrix m n R<VAR>hA : Continuous A<VAR>hB : Continuous B<GOAL>Continuous fun x => A x ᵥ* B x
<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₁ : m → l<VAR>e₂ : p → n<GOAL>Continuous fun x => (A x).submatrix e₁ e₂