ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>f : α →o β<VAR>b : β<GOAL>b ∈ c.map f → ∃ a ∈ c, f a = b
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>f : α →o β<VAR>b : β<GOAL>b ∈ c.map f ↔ ∃ a ∈ c, f a = b
<VAR>α : Type u<VAR>Preorder α<VAR>c : OmegaCompletePartialOrder.Chain α<GOAL>c.map OrderHom.id = c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>f : α →o β<VAR>g : β →o γ<GOAL>(c.map f).map g = c.map (g.comp f)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>f g : α →o β<VAR>h : f ≤ g<GOAL>c.map f ≤ c.map g
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>c₀ : OmegaCompletePartialOrder.Chain α<VAR>c₁ : OmegaCompletePartialOrder.Chain β<VAR>n : ℕ<GOAL>(c₀.zip c₁) n = (c₀ n, c₁ n)
<VAR>α : Type u_1<VAR>self : OmegaCompletePartialOrder α<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>i : ℕ<GOAL>c i ≤ OmegaCompletePartialOrder.ωSup c
<VAR>α : Type u_1<VAR>self : OmegaCompletePartialOrder α<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>x : α<GOAL>(∀ (i : ℕ), c i ≤ x) → OmegaCompletePartialOrder.ωSup c ≤ x
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>x : α<VAR>i : ℕ<VAR>h : x ≤ c i<GOAL>x ≤ OmegaCompletePartialOrder.ωSup c
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>x : α<VAR>h : ∀ (i : ℕ), c i ≤ x ∨ x ≤ c i<GOAL>OmegaCompletePartialOrder.ωSup c ≤ x ∨ x ≤ OmegaCompletePartialOrder.ωSup c
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>c₀ c₁ : OmegaCompletePartialOrder.Chain α<VAR>h : c₀ ≤ c₁<GOAL>OmegaCompletePartialOrder.ωSup c₀ ≤ OmegaCompletePartialOrder.ωSup c₁
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>x : α<GOAL>OmegaCompletePartialOrder.ωSup c ≤ x ↔ ∀ (i : ℕ), c i ≤ x
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>c : OmegaCompletePartialOrder.Chain α<GOAL>IsLUB (Set.range ⇑c) (OmegaCompletePartialOrder.ωSup c)
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>a : α<VAR>h : IsLUB (Set.range ⇑c) a<GOAL>a = OmegaCompletePartialOrder.ωSup c
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>f : α → β<VAR>hf : ScottContinuous f<GOAL>IsLUB (Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })) (f (OmegaCompletePartialOrder.ωSup c))
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : α → β<VAR>hf : ScottContinuous f<GOAL>OmegaCompletePartialOrder.Continuous' f
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : α → β<VAR>hf : OmegaCompletePartialOrder.Continuous' f<GOAL>Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>hf' : OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf }<GOAL>OmegaCompletePartialOrder.Continuous' f
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : α →o β<VAR>hf' : OmegaCompletePartialOrder.Continuous f<GOAL>OmegaCompletePartialOrder.Continuous' ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : α → β<VAR>hf : OmegaCompletePartialOrder.Continuous' f<GOAL>OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := ⋯ }
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : α →o β<GOAL>OmegaCompletePartialOrder.Continuous' ⇑f ↔ OmegaCompletePartialOrder.Continuous f
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<GOAL>OmegaCompletePartialOrder.Continuous OrderHom.id
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>OmegaCompletePartialOrder γ<VAR>f : α →o β<VAR>g : β →o γ<VAR>hfc : OmegaCompletePartialOrder.Continuous f<VAR>hgc : OmegaCompletePartialOrder.Continuous g<GOAL>OmegaCompletePartialOrder.Continuous (g.comp f)
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<GOAL>OmegaCompletePartialOrder.Continuous' id
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>x : β<GOAL>OmegaCompletePartialOrder.Continuous ((OrderHom.const α) x)
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>x : β<GOAL>OmegaCompletePartialOrder.Continuous' (Function.const α x)
<VAR>α : Type u<VAR>c : OmegaCompletePartialOrder.Chain (Part α)<VAR>a b : α<VAR>ha : Part.some a ∈ c<VAR>hb : Part.some b ∈ c<GOAL>a = b
<VAR>α : Type u<VAR>c : OmegaCompletePartialOrder.Chain (Part α)<VAR>a : α<VAR>h : Part.some a ∈ c<GOAL>Part.ωSup c = Part.some a
<VAR>α : Type u<VAR>c : OmegaCompletePartialOrder.Chain (Part α)<VAR>h : ¬∃ a, Part.some a ∈ c<GOAL>Part.ωSup c = Part.none
<VAR>α : Type u<VAR>c : OmegaCompletePartialOrder.Chain (Part α)<VAR>a : α<VAR>h : a ∈ Part.ωSup c<GOAL>Part.some a ∈ c
<VAR>α : Type u<VAR>x : α<VAR>c : OmegaCompletePartialOrder.Chain (Part α)<GOAL>x ∈ OmegaCompletePartialOrder.ωSup c ↔ Part.some x ∈ c
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : Type u_3<VAR>(x : α) → OmegaCompletePartialOrder (β x)<VAR>OmegaCompletePartialOrder γ<VAR>f : (x : α) → γ → β x<VAR>a : α<VAR>hf : OmegaCompletePartialOrder.Continuous' fun x y => f y x<GOAL>OmegaCompletePartialOrder.Continuous' (f a)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : Type u_3<VAR>(x : α) → OmegaCompletePartialOrder (β x)<VAR>OmegaCompletePartialOrder γ<VAR>f : γ → (x : α) → β x<VAR>hf : ∀ (x : α), OmegaCompletePartialOrder.Continuous' fun g => f g x<GOAL>OmegaCompletePartialOrder.Continuous' f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c : OmegaCompletePartialOrder.Chain (α × β)<GOAL>(Prod.ωSup c).2 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c : OmegaCompletePartialOrder.Chain (α × β)<GOAL>(Prod.ωSup c).1 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.fst)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c : OmegaCompletePartialOrder.Chain (α × β)<GOAL>(OmegaCompletePartialOrder.ωSup c).1 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.fst)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c : OmegaCompletePartialOrder.Chain (α × β)<GOAL>(OmegaCompletePartialOrder.ωSup c).2 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c₀ : OmegaCompletePartialOrder.Chain α<VAR>c₁ : OmegaCompletePartialOrder.Chain β<GOAL>OmegaCompletePartialOrder.ωSup (c₀.zip c₁) = (OmegaCompletePartialOrder.ωSup c₀, OmegaCompletePartialOrder.ωSup c₁)
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>CompleteLattice β<VAR>s : Set (α →o β)<VAR>hs : ∀ f ∈ s, OmegaCompletePartialOrder.Continuous f<GOAL>OmegaCompletePartialOrder.Continuous (sSup s)
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>CompleteLattice β<VAR>ι : Sort u_1<VAR>f : ι → α →o β<VAR>h : ∀ (i : ι), OmegaCompletePartialOrder.Continuous (f i)<GOAL>OmegaCompletePartialOrder.Continuous (⨆ i, f i)
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>CompleteLattice β<VAR>s : Set (α → β)<VAR>hc : ∀ f ∈ s, OmegaCompletePartialOrder.Continuous' f<GOAL>OmegaCompletePartialOrder.Continuous' (sSup s)
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>CompleteLattice β<VAR>f g : α →o β<VAR>hf : OmegaCompletePartialOrder.Continuous f<VAR>hg : OmegaCompletePartialOrder.Continuous g<GOAL>OmegaCompletePartialOrder.Continuous (f ⊔ g)
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>CompleteLattice β<GOAL>OmegaCompletePartialOrder.Continuous ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>CompleteLattice β<GOAL>OmegaCompletePartialOrder.Continuous ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OmegaCompletePartialOrder α<VAR>CompleteLinearOrder β<VAR>f g : α →o β<VAR>hf : OmegaCompletePartialOrder.Continuous f<VAR>hg : OmegaCompletePartialOrder.Continuous g<GOAL>OmegaCompletePartialOrder.Continuous (f ⊓ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OmegaCompletePartialOrder α<VAR>CompleteLinearOrder β<VAR>f g : α → β<VAR>hf : OmegaCompletePartialOrder.Continuous' f<VAR>hg : OmegaCompletePartialOrder.Continuous' g<GOAL>OmegaCompletePartialOrder.Continuous' (f ⊓ g)
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c : OmegaCompletePartialOrder.Chain (α →o β)<VAR>a : α<GOAL>(OmegaCompletePartialOrder.OrderHom.ωSup c) a = OmegaCompletePartialOrder.ωSup (c.map (OrderHom.apply a))
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c : OmegaCompletePartialOrder.Chain (α →o β)<VAR>a : α<GOAL>(OmegaCompletePartialOrder.ωSup c) a = OmegaCompletePartialOrder.ωSup (c.map (OrderHom.apply a))
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>self : α →𝒄 β<GOAL>OmegaCompletePartialOrder.Continuous self.toOrderHom
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : α →𝒄 β<GOAL>f.toOrderHom = ↑f
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : α →o β<VAR>hf : OmegaCompletePartialOrder.Continuous f<GOAL>⇑{ toOrderHom := f, cont := hf } = ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : α →𝒄 β<GOAL>⇑f.toOrderHom = ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f g : α →𝒄 β<VAR>h : f = g<VAR>x : α<GOAL>f x = g x
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : α →𝒄 β<VAR>x y : α<VAR>h : x = y<GOAL>f x = f y
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : α →𝒄 β<GOAL>Monotone ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f g : α →𝒄 β<VAR>x y : α<VAR>h₁ : f ≤ g<VAR>h₂ : x ≤ y<GOAL>f x ≤ g y
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>p : Prop<VAR>hp : Decidable p<VAR>f g : α → β<VAR>hf : OmegaCompletePartialOrder.Continuous' f<VAR>hg : OmegaCompletePartialOrder.Continuous' g<GOAL>OmegaCompletePartialOrder.Continuous' fun x => if p then f x else g x
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>β γ : Type v<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>f : α →o Part β<VAR>g : α →o β → Part γ<GOAL>OmegaCompletePartialOrder.ωSup (c.map (f.partBind g)) = OmegaCompletePartialOrder.ωSup (c.map f) >>= OmegaCompletePartialOrder.ωSup (c.map g)
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>β γ : Type v<VAR>f : α → Part β<VAR>g : α → β → Part γ<GOAL>OmegaCompletePartialOrder.Continuous' f → OmegaCompletePartialOrder.Continuous' g → OmegaCompletePartialOrder.Continuous' fun x => f x >>= g x
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>β γ : Type v<VAR>f : β → γ<VAR>g : α → Part β<VAR>hg : OmegaCompletePartialOrder.Continuous' g<GOAL>OmegaCompletePartialOrder.Continuous' fun x => f <$> g x
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>β γ : Type v<VAR>f : α → Part (β → γ)<VAR>g : α → Part β<VAR>hf : OmegaCompletePartialOrder.Continuous' f<VAR>hg : OmegaCompletePartialOrder.Continuous' g<GOAL>OmegaCompletePartialOrder.Continuous' fun x => Seq.seq (f x) fun x_1 => g x
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>F : α →𝒄 β<VAR>C : OmegaCompletePartialOrder.Chain α<GOAL>F (OmegaCompletePartialOrder.ωSup C) = OmegaCompletePartialOrder.ωSup (C.map ↑F)
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : α → β<VAR>g : α →𝒄 β<VAR>h : f = ⇑g<GOAL>∀ (a : α), (OmegaCompletePartialOrder.ContinuousHom.copy f g h) a = f a
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>a : α<GOAL>OmegaCompletePartialOrder.ContinuousHom.id a = a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_3<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>OmegaCompletePartialOrder γ<VAR>f : β →𝒄 γ<VAR>g : α →𝒄 β<GOAL>∀ (a : α), (f.comp g) a = f (g a)
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f g : α →𝒄 β<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f g : α →𝒄 β<VAR>h : ⇑f = ⇑g<GOAL>f = g
<VAR>β : Type v<VAR>γ : Type u_3<VAR>OmegaCompletePartialOrder β<VAR>OmegaCompletePartialOrder γ<VAR>f : β →𝒄 γ<GOAL>f.comp OmegaCompletePartialOrder.ContinuousHom.id = f
<VAR>β : Type v<VAR>γ : Type u_3<VAR>OmegaCompletePartialOrder β<VAR>OmegaCompletePartialOrder γ<VAR>f : β →𝒄 γ<GOAL>OmegaCompletePartialOrder.ContinuousHom.id.comp f = f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_3<VAR>φ : Type u_4<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>OmegaCompletePartialOrder γ<VAR>OmegaCompletePartialOrder φ<VAR>f : γ →𝒄 φ<VAR>g : β →𝒄 γ<VAR>h : α →𝒄 β<GOAL>f.comp (g.comp h) = (f.comp g).comp h
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>a : α<VAR>f : α →𝒄 β<GOAL>↑f a = f a
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>x : β<GOAL>∀ (a : α), (OmegaCompletePartialOrder.ContinuousHom.const x) a = x
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : α →𝒄 β<GOAL>OmegaCompletePartialOrder.ContinuousHom.toMono f = ↑f
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)<VAR>c₁ : OmegaCompletePartialOrder.Chain α<VAR>z : β<GOAL>(∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z) ↔ ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)<VAR>c₁ : OmegaCompletePartialOrder.Chain α<VAR>z : β<GOAL>(∀ (j i : ℕ), (c₀ i) (c₁ j) ≤ z) ↔ ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c : OmegaCompletePartialOrder.Chain (α →𝒄 β)<VAR>a : α<GOAL>(OmegaCompletePartialOrder.ContinuousHom.ωSup c) a = OmegaCompletePartialOrder.ωSup ((c.map OmegaCompletePartialOrder.ContinuousHom.toMono).map (OrderHom.apply a))
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c : OmegaCompletePartialOrder.Chain (α →𝒄 β)<GOAL>OmegaCompletePartialOrder.ωSup c = OmegaCompletePartialOrder.ContinuousHom.ωSup c
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>f : (α →𝒄 β) × α<GOAL>OmegaCompletePartialOrder.ContinuousHom.Prod.apply f = f.1 f.2
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c : OmegaCompletePartialOrder.Chain (α →𝒄 β)<VAR>x : α<GOAL>(OmegaCompletePartialOrder.ωSup c) x = (OmegaCompletePartialOrder.ContinuousHom.ωSup c) x
<VAR>α : Type u<VAR>β : Type v<VAR>OmegaCompletePartialOrder α<VAR>OmegaCompletePartialOrder β<VAR>c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)<VAR>c₁ : OmegaCompletePartialOrder.Chain α<GOAL>(OmegaCompletePartialOrder.ωSup c₀) (OmegaCompletePartialOrder.ωSup c₁) = OmegaCompletePartialOrder.ContinuousHom.Prod.apply (OmegaCompletePartialOrder.ωSup (c₀.zip c₁))
<VAR>β : Type v<VAR>γ : Type u_3<VAR>OmegaCompletePartialOrder β<VAR>OmegaCompletePartialOrder γ<VAR>α : Type u_5<VAR>f : α → β →𝒄 γ<VAR>x : β<VAR>y : α<GOAL>(OmegaCompletePartialOrder.ContinuousHom.flip f) x y = (f y) x
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>β γ : Type v<VAR>f : α →𝒄 Part β<VAR>g : α →𝒄 β → Part γ<VAR>x : α<GOAL>(f.bind g) x = (f x).bind (g x)
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>β γ : Type v<VAR>f : β → γ<VAR>g : α →𝒄 Part β<VAR>x : α<GOAL>(OmegaCompletePartialOrder.ContinuousHom.map f g) x = Part.map f (g x)
<VAR>α : Type u<VAR>OmegaCompletePartialOrder α<VAR>β γ : Type v<VAR>f : α →𝒄 Part (β → γ)<VAR>g : α →𝒄 Part β<VAR>x : α<GOAL>(f.seq g) x = Seq.seq (f x) fun x_1 => g x
<VAR>α : Type u_2<VAR>f : Filter α<GOAL>f.ker = ⋂ s ∈ f, s
<VAR>α : Type u_2<VAR>f : Filter α<VAR>a : α<GOAL>a ∈ f.ker ↔ ∀ s ∈ f, a ∈ s
<VAR>α : Type u_2<VAR>f : Filter α<VAR>s : Set α<GOAL>s ⊆ f.ker ↔ ∀ t ∈ f, s ⊆ t
<VAR>α : Type u_2<GOAL>Function.Surjective Filter.ker
<VAR>α : Type u_2<GOAL>⊥.ker = ∅
<VAR>α : Type u_2<GOAL>⊤.ker = Set.univ
<VAR>α : Type u_2<VAR>f : Filter α<GOAL>f.ker = Set.univ ↔ f = ⊤
<VAR>α : Type u_2<VAR>f g : Filter α<GOAL>(f ⊓ g).ker = f.ker ∩ g.ker
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>f : ι → Filter α<GOAL>(⨅ i, f i).ker = ⨅ i, (f i).ker
<VAR>α : Type u_2<VAR>S : Set (Filter α)<GOAL>(sInf S).ker = ⨅ f ∈ S, f.ker
<VAR>α : Type u_2<VAR>s : Set α<GOAL>(Filter.principal s).ker = s
<VAR>α : Type u_2<VAR>a : α<GOAL>(pure a).ker = {a}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m : α → β<VAR>f : Filter β<GOAL>(Filter.comap m f).ker = m ⁻¹' f.ker
<VAR>n : ℕ<VAR>h : n ≠ 0<VAR>d : ℕ<GOAL>∃ᶠ (m : ℕ) in Filter.atTop, m ≡ d [MOD n]
<VAR>d n : ℕ<VAR>h : d < n<GOAL>∃ᶠ (m : ℕ) in Filter.atTop, m % n = d
<GOAL>∃ᶠ (m : ℕ) in Filter.atTop, Even m
<GOAL>∃ᶠ (m : ℕ) in Filter.atTop, Odd m
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a : α<VAR>h : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ a ^ n<GOAL>0 ≤ a
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Preorder α<VAR>Preorder β<VAR>self : α →o β<GOAL>Monotone self.toFun
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>LE α<VAR>LE β<VAR>EquivLike F α β<VAR>self : OrderIsoClass F α β<VAR>f : F<VAR>a b : α<GOAL>f a ≤ f b ↔ a ≤ b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>FunLike F α β<VAR>OrderHomClass F α β<VAR>f : F<GOAL>Monotone ⇑f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>EquivLike F α β<VAR>OrderIsoClass F α β<VAR>f : F<VAR>a : α<VAR>b : β<GOAL>EquivLike.inv f b ≤ a ↔ b ≤ f a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>EquivLike F α β<VAR>OrderIsoClass F α β<VAR>f : F<VAR>a : α<VAR>b : β<GOAL>a ≤ EquivLike.inv f b ↔ f a ≤ b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>EquivLike F α β<VAR>OrderIsoClass F α β<VAR>f : F<VAR>a b : α<GOAL>f a < f b ↔ a < b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>EquivLike F α β<VAR>OrderIsoClass F α β<VAR>f : F<VAR>a : α<VAR>b : β<GOAL>EquivLike.inv f b < a ↔ b < f a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>EquivLike F α β<VAR>OrderIsoClass F α β<VAR>f : F<VAR>a : α<VAR>b : β<GOAL>a < EquivLike.inv f b ↔ f a < b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>⇑{ toFun := f, monotone' := hf } = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<GOAL>Monotone ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f g : α →o β<VAR>h : ⇑f = ⇑g<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<GOAL>↑f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>F : Type u_6<VAR>FunLike F α β<VAR>OrderHomClass F α β<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<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 : α →o β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>Preorder α<GOAL>⇑OrderHom.id = id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f g : α →o β<GOAL>f ≤ g ↔ ∀ (x : α), f x ≤ g x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f g : α →o β<GOAL>⇑f ≤ ⇑g ↔ f ≤ g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>{ toFun := f, monotone' := hf } ≤ { toFun := g, monotone' := hg } ↔ f ≤ g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f g : α →o β<VAR>x y : α<VAR>h₁ : f ≤ g<VAR>h₂ : x ≤ y<GOAL>f x ≤ g y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α × β →o γ<VAR>x : α<VAR>y : β<GOAL>((OrderHom.curry f) x) y = f (x, y)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α →o β →o γ<VAR>x : α × β<GOAL>((RelIso.symm OrderHom.curry) f) x = (f x.1) x.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β →o γ<VAR>f : α →o β<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₁ g₂ : β →o γ<VAR>hg : g₁ ≤ g₂<VAR>f₁ f₂ : α →o β<VAR>hf : f₁ ≤ f₂<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 : β → γ<VAR>f : α → β<VAR>hg : Monotone g<VAR>hf : Monotone f<GOAL>{ toFun := g, monotone' := hg }.comp { toFun := f, monotone' := hf } = { toFun := g ∘ f, monotone' := ⋯ }
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>x : β →o γ<GOAL>∀ (a : α →o β), ⇑((OrderHom.compₘ x) a) = ⇑x ∘ ⇑a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<GOAL>f.comp OrderHom.id = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<GOAL>OrderHom.id.comp f = f
<VAR>α : Type u_6<VAR>Preorder α<VAR>β : Type u_7<VAR>Preorder β<VAR>b : β<GOAL>⇑((OrderHom.const α) b) = Function.const α b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α →o β<VAR>c : γ<GOAL>((OrderHom.const β) c).comp f = (OrderHom.const α) c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>γ : Type u_6<VAR>Preorder γ<VAR>f : α →o β<VAR>c : α<GOAL>f.comp ((OrderHom.const γ) c) = (OrderHom.const γ) (f c)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α →o β<VAR>g : α →o γ<VAR>x : α<GOAL>(f.prod g) x = (f x, g x)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f₁ f₂ : α →o β<VAR>hf : f₁ ≤ f₂<VAR>g₁ g₂ : α →o γ<VAR>hg : g₁ ≤ g₂<GOAL>f₁.prod g₁ ≤ f₂.prod g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f₁ f₂ : β →o γ<VAR>g : α →o β<GOAL>(f₁.comp g).prod (f₂.comp g) = (f₁.prod f₂).comp g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>x : α →o β<GOAL>∀ (a : α →o γ) (x_1 : α), ((OrderHom.prodₘ x) a) x_1 = (x x_1, a x_1)
<VAR>α : Type u_2<VAR>Preorder α<VAR>x : α<GOAL>OrderHom.diag x = (x, x)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o α →o β<GOAL>∀ (a : α), f.onDiag a = (f a) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>self : α × β<GOAL>OrderHom.fst self = self.1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>self : α × β<GOAL>OrderHom.snd self = self.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<GOAL>OrderHom.fst.prod OrderHom.snd = OrderHom.id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α →o β<VAR>g : α →o γ<GOAL>OrderHom.fst.comp (f.prod g) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α →o β<VAR>g : α →o γ<GOAL>OrderHom.snd.comp (f.prod g) = g