ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>f₁ f₂ : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>hl : f₁ =ᶠ[l₁] f₂<VAR>h : Filter.Tendsto f₁ l₁ l₂<GOAL>Filter.Tendsto f₂ l₁ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>f₁ f₂ : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>h : ∀ (x : α), f₁ x = f₂ x<GOAL>Filter.Tendsto f₁ l₁ l₂ ↔ Filter.Tendsto f₂ l₁ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>f₁ f₂ : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>h : ∀ (x : α), f₁ x = f₂ x<GOAL>Filter.Tendsto f₁ l₁ l₂ → Filter.Tendsto f₂ l₁ l₂
<VAR>α : Type u<VAR>x y : Filter α<GOAL>Filter.Tendsto id x y ↔ x ≤ y
<VAR>α : Type u<VAR>x : Filter α<GOAL>Filter.Tendsto id x x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>x : Filter α<VAR>y : Filter β<VAR>z : Filter γ<VAR>hg : Filter.Tendsto g y z<VAR>hf : Filter.Tendsto f x y<GOAL>Filter.Tendsto (g ∘ f) x z
<VAR>α : Type u<VAR>f : α → α<VAR>l : Filter α<VAR>h : Filter.Tendsto f l l<VAR>n : ℕ<GOAL>Filter.Tendsto f^[n] l l
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x y : Filter α<VAR>z : Filter β<VAR>hx : Filter.Tendsto f x z<VAR>h : y ≤ x<GOAL>Filter.Tendsto f y z
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : Filter α<VAR>y z : Filter β<VAR>hy : Filter.Tendsto f x y<VAR>hz : y ≤ z<GOAL>Filter.Tendsto f x z
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : Filter α<VAR>y : Filter β<VAR>h : Filter.Tendsto f x y<VAR>hx : x.NeBot<GOAL>y.NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : Filter α<GOAL>Filter.Tendsto f x (Filter.map f x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : β → γ<VAR>g : α → β<VAR>x : Filter α<VAR>y : Filter γ<GOAL>Filter.Tendsto f (Filter.map g x) y ↔ Filter.Tendsto (f ∘ g) x y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : Filter β<GOAL>Filter.Tendsto f (Filter.comap f x) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>a : Filter α<VAR>c : Filter γ<GOAL>Filter.Tendsto f a (Filter.comap g c) ↔ Filter.Tendsto (g ∘ f) a c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>m : α → β<VAR>f : Filter α<VAR>g : Filter β<VAR>i : γ → α<VAR>h : Set.range i ∈ f<GOAL>Filter.Tendsto (m ∘ i) (Filter.comap i f) g ↔ Filter.Tendsto m f g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>a : Filter α<VAR>b : Filter β<VAR>c : Filter γ<VAR>hfg : Filter.Tendsto (g ∘ f) a c<VAR>hg : Filter.comap g c ≤ b<GOAL>Filter.Tendsto f a b
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>g : Filter β<VAR>φ : α → β<VAR>ψ : β → α<VAR>eq : ψ ∘ φ = id<VAR>hφ : Filter.Tendsto φ f g<VAR>hψ : Filter.Tendsto ψ g f<GOAL>Filter.comap φ g = f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>g : Filter β<VAR>φ : α → β<VAR>ψ : β → α<VAR>eq : φ ∘ ψ = id<VAR>hφ : Filter.Tendsto φ f g<VAR>hψ : Filter.Tendsto ψ g f<GOAL>Filter.map φ f = g
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : Filter α<VAR>y₁ y₂ : Filter β<GOAL>Filter.Tendsto f x (y₁ ⊓ y₂) ↔ Filter.Tendsto f x y₁ ∧ Filter.Tendsto f x y₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x₁ x₂ : Filter α<VAR>y : Filter β<VAR>h : Filter.Tendsto f x₁ y<GOAL>Filter.Tendsto f (x₁ ⊓ x₂) y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x₁ x₂ : Filter α<VAR>y : Filter β<VAR>h : Filter.Tendsto f x₂ y<GOAL>Filter.Tendsto f (x₁ ⊓ x₂) y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x₁ x₂ : Filter α<VAR>y₁ y₂ : Filter β<VAR>h₁ : Filter.Tendsto f x₁ y₁<VAR>h₂ : Filter.Tendsto f x₂ y₂<GOAL>Filter.Tendsto f (x₁ ⊓ x₂) (y₁ ⊓ y₂)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>f : α → β<VAR>x : Filter α<VAR>y : ι → Filter β<GOAL>Filter.Tendsto f x (⨅ i, y i) ↔ ∀ (i : ι), Filter.Tendsto f x (y i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>f : α → β<VAR>x : ι → Filter α<VAR>y : Filter β<VAR>i : ι<VAR>hi : Filter.Tendsto f (x i) y<GOAL>Filter.Tendsto f (⨅ i, x i) y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>f : α → β<VAR>x : ι → Filter α<VAR>y : ι → Filter β<VAR>h : ∀ (i : ι), Filter.Tendsto f (x i) (y i)<GOAL>Filter.Tendsto f (iInf x) (iInf y)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x₁ x₂ : Filter α<VAR>y : Filter β<GOAL>Filter.Tendsto f (x₁ ⊔ x₂) y ↔ Filter.Tendsto f x₁ y ∧ Filter.Tendsto f x₂ y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x₁ x₂ : Filter α<VAR>y : Filter β<GOAL>Filter.Tendsto f x₁ y → Filter.Tendsto f x₂ y → Filter.Tendsto f (x₁ ⊔ x₂) y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x₁ x₂ : Filter α<VAR>y₁ y₂ : Filter β<VAR>h₁ : Filter.Tendsto f x₁ y₁<VAR>h₂ : Filter.Tendsto f x₂ y₂<GOAL>Filter.Tendsto f (x₁ ⊔ x₂) (y₁ ⊔ y₂)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>f : α → β<VAR>x : ι → Filter α<VAR>y : Filter β<GOAL>Filter.Tendsto f (⨆ i, x i) y ↔ ∀ (i : ι), Filter.Tendsto f (x i) y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>f : α → β<VAR>x : ι → Filter α<VAR>y : ι → Filter β<VAR>h : ∀ (i : ι), Filter.Tendsto f (x i) (y i)<GOAL>Filter.Tendsto f (iSup x) (iSup y)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : Filter α<VAR>s : Set β<GOAL>Filter.Tendsto f l (𝓟 s) ↔ ∀ᶠ (a : α) in l, f a ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>Filter.Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ a ∈ s, f a ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : Filter α<VAR>b : β<GOAL>Filter.Tendsto f a (pure b) ↔ ∀ᶠ (x : α) in a, f x = b
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<GOAL>Filter.Tendsto f (pure a) (pure (f a))
<VAR>α : Type u<VAR>β : Type v<VAR>a : Filter α<VAR>b : β<GOAL>Filter.Tendsto (fun x => b) a (pure b)
<VAR>α : Type u<VAR>a : α<VAR>l : Filter α<GOAL>pure a ≤ l ↔ ∀ s ∈ l, a ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<VAR>l : Filter β<GOAL>Filter.Tendsto f (pure a) l ↔ ∀ s ∈ l, f a ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>l : Filter α<GOAL>Filter.map f (l ⊓ 𝓟 (f ⁻¹' s)) = Filter.map f l ⊓ 𝓟 s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : Filter α<VAR>b₁ b₂ : Filter β<VAR>hf : Filter.Tendsto f a b₁<VAR>a.NeBot<VAR>hb : Disjoint b₁ b₂<GOAL>¬Filter.Tendsto f a b₂
<VAR>α : Type u<VAR>β : Type v<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>f g : α → β<VAR>p : α → Prop<VAR>(x : α) → Decidable (p x)<VAR>h₀ : Filter.Tendsto f (l₁ ⊓ 𝓟 {x | p x}) l₂<VAR>h₁ : Filter.Tendsto g (l₁ ⊓ 𝓟 {x | ¬p x}) l₂<GOAL>Filter.Tendsto (fun x => if p x then f x else g x) l₁ l₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>f g : α → β<VAR>p : α → Prop<VAR>DecidablePred p<VAR>hf : Filter.Tendsto f l₁ l₂<VAR>hg : Filter.Tendsto g l₁ l₂<GOAL>Filter.Tendsto (fun a => if p a then f a else g a) l₁ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>f g : α → β<VAR>s : Set α<VAR>(x : α) → Decidable (x ∈ s)<VAR>h₀ : Filter.Tendsto f (l₁ ⊓ 𝓟 s) l₂<VAR>h₁ : Filter.Tendsto g (l₁ ⊓ 𝓟 sᶜ) l₂<GOAL>Filter.Tendsto (s.piecewise f g) l₁ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f g : α → β<VAR>h : Set.EqOn f g s<GOAL>f =ᶠ[𝓟 s] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>l : Filter α<VAR>f g : α → β<VAR>h : Set.EqOn f g s<VAR>hl : s ∈ l<GOAL>f =ᶠ[l] g
<VAR>α : Type u_1<VAR>l : Filter α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>s ≤ᶠ[l] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : Set.MapsTo f s t<GOAL>Filter.Tendsto f (𝓟 s) (𝓟 t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>f f' : α → β<VAR>H : f =ᶠ[l] f'<VAR>g : γ → α<VAR>lc : Filter γ<VAR>hg : Filter.Tendsto g lc l<GOAL>f ∘ g =ᶠ[lc] f' ∘ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Filter α<VAR>G : Filter β<VAR>m : α → β<GOAL>Set.MapsTo (Filter.map m) (Set.Iic F) (Set.Iic G) ↔ Filter.Tendsto m F G
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>m : α → β<GOAL>Set.MapsTo (Filter.map m) (Set.Iic (𝓟 s)) (Set.Iic (𝓟 t)) ↔ Set.MapsTo m s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Filter α<VAR>G : Filter β<VAR>m : α → β<GOAL>Set.SurjOn (Filter.map m) (Set.Iic F) (Set.Iic G) ↔ G ≤ Filter.map m F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>m : α → β<GOAL>Set.SurjOn (Filter.map m) (Set.Iic (𝓟 s)) (Set.Iic (𝓟 t)) ↔ Set.SurjOn m s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>m : α → β<GOAL>Set.InjOn (Filter.map m) (Set.Iic (𝓟 s)) ↔ Set.InjOn m s
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>he : p ∅<VAR>hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s<VAR>hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)<VAR>s : Set α<GOAL>s ∈ Filter.comk p he hmono hunion ↔ p sᶜ
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>he : p ∅<VAR>hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s<VAR>hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)<VAR>s : Set α<GOAL>sᶜ ∈ Filter.comk p he hmono hunion ↔ p s
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>h : ∀ i ∈ Set.Ico n m, r i (Order.succ i)<VAR>hnm : n ≤ m<GOAL>Relation.ReflTransGen r n m
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>h : ∀ i ∈ Set.Ico m n, r (Order.succ i) i<VAR>hmn : m ≤ n<GOAL>Relation.ReflTransGen r n m
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>h : ∀ i ∈ Set.Ico n m, r i (Order.succ i)<VAR>hnm : n < m<GOAL>Relation.TransGen r n m
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>h : ∀ i ∈ Set.Ico m n, r (Order.succ i) i<VAR>hmn : m < n<GOAL>Relation.TransGen r n m
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>h1 : ∀ i ∈ Set.Ico n m, r i (Order.succ i)<VAR>h2 : ∀ i ∈ Set.Ico m n, r (Order.succ i) i<GOAL>Relation.ReflTransGen r n m
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>h1 : ∀ i ∈ Set.Ico n m, r i (Order.succ i)<VAR>h2 : ∀ i ∈ Set.Ico m n, r (Order.succ i) i<VAR>hnm : n ≠ m<GOAL>Relation.TransGen r n m
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>hr : Reflexive r<VAR>h1 : ∀ i ∈ Set.Ico n m, r i (Order.succ i)<VAR>h2 : ∀ i ∈ Set.Ico m n, r (Order.succ i) i<GOAL>Relation.TransGen r n m
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>h : ∀ i ∈ Set.Ioc m n, r i (Order.pred i)<VAR>hnm : m ≤ n<GOAL>Relation.ReflTransGen r n m
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>h : ∀ i ∈ Set.Ioc n m, r (Order.pred i) i<VAR>hmn : n ≤ m<GOAL>Relation.ReflTransGen r n m
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>h : ∀ i ∈ Set.Ioc m n, r i (Order.pred i)<VAR>hnm : m < n<GOAL>Relation.TransGen r n m
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>h : ∀ i ∈ Set.Ioc n m, r (Order.pred i) i<VAR>hmn : n < m<GOAL>Relation.TransGen r n m
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>h1 : ∀ i ∈ Set.Ioc m n, r i (Order.pred i)<VAR>h2 : ∀ i ∈ Set.Ioc n m, r (Order.pred i) i<GOAL>Relation.ReflTransGen r n m
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>h1 : ∀ i ∈ Set.Ioc m n, r i (Order.pred i)<VAR>h2 : ∀ i ∈ Set.Ioc n m, r (Order.pred i) i<VAR>hnm : n ≠ m<GOAL>Relation.TransGen r n m
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>hr : Reflexive r<VAR>h1 : ∀ i ∈ Set.Ioc m n, r i (Order.pred i)<VAR>h2 : ∀ i ∈ Set.Ioc n m, r (Order.pred i) i<GOAL>Relation.TransGen r n m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>LinearOrder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>m n : α<GOAL>⋃ i ∈ Set.Ico m n, Set.Ioc (f i) (f (Order.succ i)) = Set.Ioc (f m) (f n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>SuccOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Pairwise (Disjoint on fun n => Set.Ioc (f n) (f (Order.succ n)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>SuccOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Pairwise (Disjoint on fun n => Set.Ico (f n) (f (Order.succ n)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>SuccOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Pairwise (Disjoint on fun n => Set.Ioo (f n) (f (Order.succ n)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PredOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Pairwise (Disjoint on fun n => Set.Ioc (f (Order.pred n)) (f n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PredOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Pairwise (Disjoint on fun n => Set.Ico (f (Order.pred n)) (f n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PredOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Pairwise (Disjoint on fun n => Set.Ioo (f (Order.pred n)) (f n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>SuccOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Pairwise (Disjoint on fun n => Set.Ioc (f (Order.succ n)) (f n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>SuccOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Pairwise (Disjoint on fun n => Set.Ico (f (Order.succ n)) (f n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>SuccOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Pairwise (Disjoint on fun n => Set.Ioo (f (Order.succ n)) (f n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PredOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Pairwise (Disjoint on fun n => Set.Ioc (f n) (f (Order.pred n)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PredOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Pairwise (Disjoint on fun n => Set.Ico (f n) (f (Order.pred n)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>PredOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Pairwise (Disjoint on fun n => Set.Ioo (f n) (f (Order.pred n)))
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<GOAL>↑(BddLat.of α).toLat = α
<VAR>X : BddLat<GOAL>↑((CategoryTheory.forget₂ BddLat BddOrd).obj X).toPartOrd = ↑X.toLat
<VAR>X : BddLat<GOAL>↑((CategoryTheory.forget₂ BddLat Lat).obj X) = ↑X.toLat
<VAR>X : BddLat<GOAL>((CategoryTheory.forget₂ BddLat SemilatSupCat).obj X).X = ↑X.toLat
<VAR>X : BddLat<GOAL>((CategoryTheory.forget₂ BddLat SemilatInfCat).obj X).X = ↑X.toLat
<GOAL>CategoryTheory.forget₂ BddLat Lat ⋙ CategoryTheory.forget₂ Lat PartOrd = CategoryTheory.forget₂ BddLat BddOrd ⋙ CategoryTheory.forget₂ BddOrd PartOrd
<GOAL>CategoryTheory.forget₂ BddLat SemilatSupCat ⋙ CategoryTheory.forget₂ SemilatSupCat PartOrd = CategoryTheory.forget₂ BddLat BddOrd ⋙ CategoryTheory.forget₂ BddOrd PartOrd
<GOAL>CategoryTheory.forget₂ BddLat SemilatInfCat ⋙ CategoryTheory.forget₂ SemilatInfCat PartOrd = CategoryTheory.forget₂ BddLat BddOrd ⋙ CategoryTheory.forget₂ BddOrd PartOrd
<VAR>α β : BddLat<VAR>e : ↑α.toLat ≃o ↑β.toLat<VAR>a : ↑β.toLat<GOAL>(BddLat.Iso.mk e).inv.toSupHom a = e.symm a
<VAR>α β : BddLat<VAR>e : ↑α.toLat ≃o ↑β.toLat<VAR>a : ↑α.toLat<GOAL>(BddLat.Iso.mk e).hom.toSupHom a = e a
<VAR>X : BddLat<GOAL>BddLat.dual.obj X = BddLat.of (↑X.toLat)ᵒᵈ
<VAR>X Y : BddLat<VAR>a : BoundedLatticeHom ↑X.toLat ↑Y.toLat<GOAL>BddLat.dual.map a = BoundedLatticeHom.dual a
<GOAL>BddLat.dualEquiv.functor = BddLat.dual
<GOAL>BddLat.dualEquiv.inverse = BddLat.dual
<GOAL>BddLat.dual ⋙ CategoryTheory.forget₂ BddLat BddOrd = CategoryTheory.forget₂ BddLat BddOrd ⋙ BddOrd.dual
<GOAL>BddLat.dual ⋙ CategoryTheory.forget₂ BddLat Lat = CategoryTheory.forget₂ BddLat Lat ⋙ Lat.dual
<GOAL>BddLat.dual ⋙ CategoryTheory.forget₂ BddLat SemilatSupCat = CategoryTheory.forget₂ BddLat SemilatInfCat ⋙ SemilatInfCat.dual
<GOAL>BddLat.dual ⋙ CategoryTheory.forget₂ BddLat SemilatInfCat = CategoryTheory.forget₂ BddLat SemilatSupCat ⋙ SemilatSupCat.dual
<VAR>α : Type u_1<VAR>self : NonemptyFiniteLinearOrder α<GOAL>Nonempty α
<VAR>α : Type u_1<VAR>NonemptyFiniteLinearOrder α<GOAL>↑(NonemptyFinLinOrd.of α) = α
<VAR>α β : NonemptyFinLinOrd<VAR>e : ↑α ≃o ↑β<GOAL>(NonemptyFinLinOrd.Iso.mk e).inv = ↑e.symm
<VAR>α β : NonemptyFinLinOrd<VAR>e : ↑α ≃o ↑β<GOAL>(NonemptyFinLinOrd.Iso.mk e).hom = ↑e
<VAR>X : NonemptyFinLinOrd<GOAL>NonemptyFinLinOrd.dual.obj X = NonemptyFinLinOrd.of (↑X)ᵒᵈ
<GOAL>∀ {X Y : NonemptyFinLinOrd} (a : ↑X →o ↑Y), NonemptyFinLinOrd.dual.map a = OrderHom.dual a
<GOAL>NonemptyFinLinOrd.dualEquiv.functor = NonemptyFinLinOrd.dual
<GOAL>NonemptyFinLinOrd.dualEquiv.inverse = NonemptyFinLinOrd.dual
<VAR>A B : NonemptyFinLinOrd<VAR>f : A ⟶ B<GOAL>CategoryTheory.Mono f ↔ Function.Injective ⇑f
<VAR>A B : NonemptyFinLinOrd<VAR>f : A ⟶ B<VAR>a : ↑A<GOAL>(CategoryTheory.forget NonemptyFinLinOrd).map f a = f.toFun a
<VAR>A B : NonemptyFinLinOrd<VAR>f : A ⟶ B<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑f
<GOAL>NonemptyFinLinOrd.dual ⋙ CategoryTheory.forget₂ NonemptyFinLinOrd LinOrd = CategoryTheory.forget₂ NonemptyFinLinOrd LinOrd ⋙ LinOrd.dual
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>DirectedOn r s ↔ Directed r Subtype.val
<VAR>α : Type u<VAR>ι : Sort w<VAR>r : α → α → Prop<VAR>f : ι → α<GOAL>Directed r f ↔ DirectedOn r (Set.range f)
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : Set β<VAR>f : β → α<GOAL>DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s
<VAR>α : Type u<VAR>r r' : α → α → Prop<VAR>s : Set α<VAR>hs : DirectedOn r s<VAR>h : ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b → r' a b<GOAL>DirectedOn r' s
<VAR>α : Type u<VAR>r r' : α → α → Prop<VAR>s : Set α<VAR>h : DirectedOn r s<VAR>H : ∀ ⦃a b : α⦄, r a b → r' a b<GOAL>DirectedOn r' s
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>ι : Sort u_1<VAR>f : ι → β<VAR>g : β → α<GOAL>Directed r (g ∘ f) ↔ Directed (g ⁻¹'o r) f
<VAR>α : Type u<VAR>r s : α → α → Prop<VAR>ι : Sort u_1<VAR>f : ι → α<VAR>H : ∀ (a b : α), r a b → s a b<VAR>h : Directed r f<GOAL>Directed s f
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>ι : Sort u_1<VAR>rb : β → β → Prop<VAR>g : α → β<VAR>f : ι → α<VAR>hg : ∀ ⦃x y : α⦄, r x y → rb (g x) (g y)<VAR>hf : Directed r f<GOAL>Directed rb (g ∘ f)
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>S : Set α<VAR>H : ∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊔ j ∈ S<GOAL>DirectedOn (fun x x_1 => x ≤ x_1) S
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>Preorder α<VAR>OrderBot α<VAR>e : ι → β<VAR>f : ι → α<VAR>hf : Directed (fun x x_1 => x ≤ x_1) f<VAR>he : Function.Injective e<GOAL>Directed (fun x x_1 => x ≤ x_1) (Function.extend e f ⊥)
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>S : Set α<VAR>H : ∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊓ j ∈ S<GOAL>DirectedOn (fun x x_1 => x ≥ x_1) S
<VAR>α : Type u<VAR>ι : Sort w<VAR>r : α → α → Prop<VAR>IsTotal α r<VAR>f : ι → α<GOAL>Directed r f
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>self : IsDirected α r<VAR>a b : α<GOAL>∃ c, r a c ∧ r b c
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsDirected α r<VAR>a b : α<GOAL>∃ c, r a c ∧ r b c
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsDirected α r<GOAL>Directed r id
<VAR>α : Type u<VAR>r : α → α → Prop<GOAL>Directed r id ↔ IsDirected α r
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsDirected α r<GOAL>DirectedOn r Set.univ
<VAR>α : Type u<VAR>r : α → α → Prop<GOAL>DirectedOn r Set.univ ↔ IsDirected α r
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>s : α → α → Prop<VAR>IsDirected α r<VAR>h : ∀ ⦃a b : α⦄, r a b → s a b<GOAL>IsDirected α s
<VAR>α : Type u<VAR>LE α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>∃ c, a ≤ c ∧ b ≤ c
<VAR>α : Type u<VAR>LE α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>a b : α<GOAL>∃ c ≤ a, c ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>LE α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>f : α → β<VAR>r : β → β → Prop<VAR>H : ∀ ⦃i j : α⦄, i ≤ j → r (f i) (f j)<GOAL>Directed r f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>Preorder β<VAR>f : α → β<GOAL>Monotone f → Directed (fun x x_1 => x ≤ x_1) f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Directed (fun x x_1 => x ≥ x_1) f
<VAR>α : Type u<VAR>β : Type v<VAR>LE α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>r : β → β → Prop<VAR>f : α → β<VAR>hf : ∀ (a₁ a₂ : α), a₁ ≤ a₂ → r (f a₂) (f a₁)<GOAL>Directed r f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Directed (fun x x_1 => x ≥ x_1) f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Directed (fun x x_1 => x ≤ x_1) f
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>h : Reflexive r<VAR>a : α<VAR>s : Set α<VAR>hd : DirectedOn r s<VAR>ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c<GOAL>DirectedOn r (insert a s)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>h : Reflexive r<VAR>a : α<GOAL>DirectedOn r {a}
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>h : Reflexive r<VAR>a b : α<VAR>hab : r a b<GOAL>DirectedOn r {a, b}
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>h : Reflexive r<VAR>a b : α<VAR>hab : r a b<GOAL>DirectedOn r {b, a}
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>h : IsMin a<GOAL>IsBot a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>h : IsMax a<GOAL>IsTop a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>hd : DirectedOn (fun x x_1 => x ≥ x_1) s<VAR>m : α<VAR>hm : m ∈ s<VAR>hmin : ∀ a ∈ s, a ≤ m → m ≤ a<VAR>a : α<GOAL>a ∈ s → m ≤ a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>hd : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>m : α<VAR>hm : m ∈ s<VAR>hmax : ∀ a ∈ s, m ≤ a → a ≤ m<VAR>a : α<GOAL>a ∈ s → a ≤ m
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>IsTop a ∨ ∃ b, a < b
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>a : α<GOAL>IsBot a ∨ ∃ b, b < a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<VAR>IsDirected α fun x x_1 => x ≥ x_1<GOAL>IsBot a ↔ IsMin a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<VAR>IsDirected α fun x x_1 => x ≤ x_1<GOAL>IsTop a ↔ IsMax a
<VAR>β : Type v<VAR>PartialOrder β<VAR>IsDirected β fun x x_1 => x ≥ x_1<VAR>Nontrivial β<GOAL>∃ a b, a < b
<VAR>β : Type v<VAR>PartialOrder β<VAR>IsDirected β fun x x_1 => x ≤ x_1<VAR>Nontrivial β<GOAL>∃ a b, a < b
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>PartialOrder β<VAR>f : α → β<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>hf : Monotone f<VAR>hf' : Antitone f<VAR>a b : α<GOAL>f a = f b
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>PartialOrder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>hf' : AntitoneOn f s<VAR>hs : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>a : α<GOAL>a ∈ s → ∀ ⦃b : α⦄, b ∈ s → f a = f b
<VAR>α : Type u_1<VAR>LT α<VAR>a : α<GOAL>¬Order.IsSuccLimit a ↔ ∃ b, b ⋖ a
<VAR>α : Type u_1<VAR>LT α<VAR>DenselyOrdered α<VAR>a : α<GOAL>Order.IsSuccLimit a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>IsMin a → Order.IsSuccLimit a
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<GOAL>Order.IsSuccLimit ⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>SuccOrder α<VAR>h : Order.IsSuccLimit (Order.succ a)<GOAL>IsMax a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>SuccOrder α<VAR>ha : ¬IsMax a<GOAL>¬Order.IsSuccLimit (Order.succ a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>SuccOrder α<VAR>NoMaxOrder α<VAR>h : Order.IsSuccLimit a<VAR>b : α<GOAL>Order.succ b ≠ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>¬Order.IsSuccLimit (Order.succ a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>NoMaxOrder α<VAR>h : Order.IsSuccLimit a<GOAL>IsMin a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>NoMaxOrder α<GOAL>Order.IsSuccLimit a ↔ IsMin a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>NoMinOrder α<VAR>NoMaxOrder α<GOAL>¬Order.IsSuccLimit a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>h : ∀ (b : α), Order.succ b ≠ a<GOAL>Order.IsSuccLimit a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<GOAL>¬Order.IsSuccLimit a ↔ ∃ b, ¬IsMax b ∧ Order.succ b = a