ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>A B : SemilatticeInf α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<VAR>x y : α<GOAL>x ⊓ y = x ⊓ y
<VAR>α : Type u_1<VAR>A B : SemilatticeInf α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>A = B
<VAR>α : Type u_1<VAR>H : SemilatticeInf α<GOAL>OrderDual.instSemilatticeInf αᵒᵈ = H
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>s s' : α<VAR>P : Prop<VAR>Decidable P<GOAL>s ⊓ s' ≤ if P then s else s'
<VAR>α : Type u_1<VAR>Sup α<VAR>Inf α<VAR>sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a<VAR>sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)<VAR>sup_idem : ∀ (a : α), a ⊔ a = a<VAR>inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a<VAR>inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)<VAR>inf_idem : ∀ (a : α), a ⊓ a = a<VAR>sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a<VAR>inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a<GOAL>SemilatticeSup.toPartialOrder = SemilatticeInf.toPartialOrder
<VAR>α : Type u<VAR>Lattice α<VAR>a b : α<GOAL>a ⊓ b ≤ a ⊔ b
<VAR>α : Type u<VAR>Lattice α<VAR>a b : α<GOAL>a ⊔ b ≤ a ⊓ b ↔ a = b
<VAR>α : Type u<VAR>Lattice α<VAR>a b : α<GOAL>a ⊓ b = a ⊔ b ↔ a = b
<VAR>α : Type u<VAR>Lattice α<VAR>a b : α<GOAL>a ⊔ b = a ⊓ b ↔ a = b
<VAR>α : Type u<VAR>Lattice α<VAR>a b : α<GOAL>a ⊓ b < a ⊔ b ↔ a ≠ b
<VAR>α : Type u<VAR>Lattice α<VAR>a b c : α<GOAL>a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c
<VAR>α : Type u<VAR>Lattice α<VAR>a b c : α<GOAL>a ⊔ b ⊓ c ≤ (a ⊔ b) ⊓ (a ⊔ c)
<VAR>α : Type u<VAR>Lattice α<VAR>a b c : α<GOAL>a ⊓ b ⊔ a ⊓ c ≤ a ⊓ (b ⊔ c)
<VAR>α : Type u<VAR>Lattice α<VAR>a b : α<GOAL>a ⊓ (a ⊔ b) = a
<VAR>α : Type u<VAR>Lattice α<VAR>a b : α<GOAL>a ⊔ a ⊓ b = a
<VAR>α : Type u<VAR>Lattice α<VAR>a b : α<GOAL>a ⊔ b = b ↔ a ⊓ b = a
<VAR>α : Type u_1<VAR>A B : Lattice α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>A = B
<VAR>α : Type u_1<VAR>self : DistribLattice α<VAR>x y z : α<GOAL>(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
<VAR>α : Type u<VAR>DistribLattice α<VAR>x y z : α<GOAL>(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
<VAR>α : Type u<VAR>DistribLattice α<VAR>a b c : α<GOAL>a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
<VAR>α : Type u<VAR>DistribLattice α<VAR>a b c : α<GOAL>a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)
<VAR>α : Type u<VAR>DistribLattice α<VAR>a b c : α<GOAL>a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c
<VAR>α : Type u<VAR>DistribLattice α<VAR>a b c : α<GOAL>(a ⊔ b) ⊓ c = a ⊓ c ⊔ b ⊓ c
<VAR>α : Type u<VAR>DistribLattice α<VAR>x y z : α<VAR>h₁ : x ⊓ z ≤ y ⊓ z<VAR>h₂ : x ⊔ z ≤ y ⊔ z<GOAL>x ≤ y
<VAR>α : Type u<VAR>DistribLattice α<VAR>a b c : α<VAR>h₁ : b ⊓ a = c ⊓ a<VAR>h₂ : b ⊔ a = c ⊔ a<GOAL>b = c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>a ⊔ b = max a b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>a ⊓ b = min a b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>p : α → Prop<VAR>ha : p a<VAR>hb : p b<GOAL>p (a ⊔ b)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>a < b ⊔ c ↔ a < b ∨ a < c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>b ⊔ c < a ↔ b < a ∧ c < a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>p : α → Prop<GOAL>p a → p b → p (a ⊓ b)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>b ⊓ c < a ↔ b < a ∨ c < a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>a < b ⊓ c ↔ a < b ∧ a < c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c d : α<GOAL>max (max a b) (max c d) = max (max a c) (max b d)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c d : α<GOAL>min (min a b) (min c d) = min (min a c) (min b d)
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>IsTotal α fun x x_1 => x ≤ x_1<GOAL>(fun x x_1 => x ⊔ x_1) = maxDefault
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>IsTotal α fun x x_1 => x ≤ x_1<GOAL>(fun x x_1 => x ⊓ x_1) = minDefault
<VAR>α : Type u<VAR>Sup α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual (a ⊓ b) = OrderDual.ofDual a ⊔ OrderDual.ofDual b
<VAR>α : Type u<VAR>Inf α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual (a ⊔ b) = OrderDual.ofDual a ⊓ OrderDual.ofDual b
<VAR>α : Type u<VAR>Inf α<VAR>a b : α<GOAL>OrderDual.toDual (a ⊓ b) = OrderDual.toDual a ⊔ OrderDual.toDual b
<VAR>α : Type u<VAR>Sup α<VAR>a b : α<GOAL>OrderDual.toDual (a ⊔ b) = OrderDual.toDual a ⊓ OrderDual.toDual b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual (min a b) = max (OrderDual.ofDual a) (OrderDual.ofDual b)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual (max a b) = min (OrderDual.ofDual a) (OrderDual.ofDual b)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>OrderDual.toDual (min a b) = max (OrderDual.toDual a) (OrderDual.toDual b)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>OrderDual.toDual (max a b) = min (OrderDual.toDual a) (OrderDual.toDual b)
<VAR>ι : Type u_1<VAR>α' : ι → Type u_2<VAR>(i : ι) → Sup (α' i)<VAR>f g : (i : ι) → α' i<VAR>i : ι<GOAL>(f ⊔ g) i = f i ⊔ g i
<VAR>ι : Type u_1<VAR>α' : ι → Type u_2<VAR>(i : ι) → Sup (α' i)<VAR>f g : (i : ι) → α' i<GOAL>f ⊔ g = fun i => f i ⊔ g i
<VAR>ι : Type u_1<VAR>α' : ι → Type u_2<VAR>(i : ι) → Inf (α' i)<VAR>f g : (i : ι) → α' i<VAR>i : ι<GOAL>(f ⊓ g) i = f i ⊓ g i
<VAR>ι : Type u_1<VAR>α' : ι → Type u_2<VAR>(i : ι) → Inf (α' i)<VAR>f g : (i : ι) → α' i<GOAL>f ⊓ g = fun i => f i ⊓ g i
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → SemilatticeSup (π i)<VAR>f : (i : ι) → π i<VAR>i : ι<VAR>a b : π i<GOAL>Function.update f i (a ⊔ b) = Function.update f i a ⊔ Function.update f i b
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → SemilatticeInf (π i)<VAR>f : (i : ι) → π i<VAR>i : ι<VAR>a b : π i<GOAL>Function.update f i (a ⊓ b) = Function.update f i a ⊓ Function.update f i b
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>SemilatticeSup β<VAR>f g : α → β<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone (f ⊔ g)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>SemilatticeInf β<VAR>f g : α → β<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone (f ⊓ g)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>LinearOrder β<VAR>f g : α → β<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun x => max (f x) (g x)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>LinearOrder β<VAR>f g : α → β<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun x => min (f x) (g x)
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>f : α → β<VAR>h : Monotone f<VAR>x y : α<GOAL>f x ⊔ f y ≤ f (x ⊔ y)
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>f : α → β<VAR>h : Monotone f<VAR>x y : α<GOAL>f (x ⊓ y) ≤ f x ⊓ f y
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>f : α → β<VAR>h : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y<GOAL>Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>f : α → β<VAR>h : ∀ (x y : α), f (x ⊔ y) = f x ⊔ f y<GOAL>Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>SemilatticeSup β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<GOAL>f (x ⊔ y) = f x ⊔ f y
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>SemilatticeInf β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<GOAL>f (x ⊓ y) = f x ⊓ f y
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>SemilatticeSup β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>hg : MonotoneOn g s<GOAL>MonotoneOn (f ⊔ g) s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>SemilatticeInf β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>hg : MonotoneOn g s<GOAL>MonotoneOn (f ⊓ g) s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>LinearOrder β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>hg : MonotoneOn g s<GOAL>MonotoneOn (fun x => max (f x) (g x)) s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>LinearOrder β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>hg : MonotoneOn g s<GOAL>MonotoneOn (fun x => min (f x) (g x)) s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊓ y) = f x ⊓ f y<GOAL>MonotoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊔ y) = f x ⊔ f y<GOAL>MonotoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<VAR>LinearOrder α<VAR>SemilatticeSup β<VAR>hf : MonotoneOn f s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f (x ⊔ y) = f x ⊔ f y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<VAR>LinearOrder α<VAR>SemilatticeInf β<VAR>hf : MonotoneOn f s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f (x ⊓ y) = f x ⊓ f y
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>SemilatticeSup β<VAR>f g : α → β<VAR>hf : Antitone f<VAR>hg : Antitone g<GOAL>Antitone (f ⊔ g)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>SemilatticeInf β<VAR>f g : α → β<VAR>hf : Antitone f<VAR>hg : Antitone g<GOAL>Antitone (f ⊓ g)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>LinearOrder β<VAR>f g : α → β<VAR>hf : Antitone f<VAR>hg : Antitone g<GOAL>Antitone fun x => max (f x) (g x)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>LinearOrder β<VAR>f g : α → β<VAR>hf : Antitone f<VAR>hg : Antitone g<GOAL>Antitone fun x => min (f x) (g x)
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup α<VAR>SemilatticeInf β<VAR>f : α → β<VAR>h : Antitone f<VAR>x y : α<GOAL>f (x ⊔ y) ≤ f x ⊓ f y
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeInf α<VAR>SemilatticeSup β<VAR>f : α → β<VAR>h : Antitone f<VAR>x y : α<GOAL>f x ⊔ f y ≤ f (x ⊓ y)
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>SemilatticeInf β<VAR>f : α → β<VAR>hf : Antitone f<VAR>x y : α<GOAL>f (x ⊔ y) = f x ⊓ f y
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>SemilatticeSup β<VAR>f : α → β<VAR>hf : Antitone f<VAR>x y : α<GOAL>f (x ⊓ y) = f x ⊔ f y
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>SemilatticeSup β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : AntitoneOn f s<VAR>hg : AntitoneOn g s<GOAL>AntitoneOn (f ⊔ g) s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>SemilatticeInf β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : AntitoneOn f s<VAR>hg : AntitoneOn g s<GOAL>AntitoneOn (f ⊓ g) s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>LinearOrder β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : AntitoneOn f s<VAR>hg : AntitoneOn g s<GOAL>AntitoneOn (fun x => max (f x) (g x)) s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>LinearOrder β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : AntitoneOn f s<VAR>hg : AntitoneOn g s<GOAL>AntitoneOn (fun x => min (f x) (g x)) s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>SemilatticeInf α<VAR>SemilatticeSup β<VAR>h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊓ y) = f x ⊔ f y<GOAL>AntitoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>SemilatticeSup α<VAR>SemilatticeInf β<VAR>h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊔ y) = f x ⊓ f y<GOAL>AntitoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<VAR>LinearOrder α<VAR>SemilatticeInf β<VAR>hf : AntitoneOn f s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f (x ⊔ y) = f x ⊓ f y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<VAR>LinearOrder α<VAR>SemilatticeSup β<VAR>hf : AntitoneOn f s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f (x ⊓ y) = f x ⊔ f y
<VAR>α : Type u<VAR>β : Type v<VAR>Sup α<VAR>Sup β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>(a₁, b₁) ⊔ (a₂, b₂) = (a₁ ⊔ a₂, b₁ ⊔ b₂)
<VAR>α : Type u<VAR>β : Type v<VAR>Inf α<VAR>Inf β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>(a₁, b₁) ⊓ (a₂, b₂) = (a₁ ⊓ a₂, b₁ ⊓ b₂)
<VAR>α : Type u<VAR>β : Type v<VAR>Sup α<VAR>Sup β<VAR>p q : α × β<GOAL>(p ⊔ q).1 = p.1 ⊔ q.1
<VAR>α : Type u<VAR>β : Type v<VAR>Inf α<VAR>Inf β<VAR>p q : α × β<GOAL>(p ⊓ q).1 = p.1 ⊓ q.1
<VAR>α : Type u<VAR>β : Type v<VAR>Sup α<VAR>Sup β<VAR>p q : α × β<GOAL>(p ⊔ q).2 = p.2 ⊔ q.2
<VAR>α : Type u<VAR>β : Type v<VAR>Inf α<VAR>Inf β<VAR>p q : α × β<GOAL>(p ⊓ q).2 = p.2 ⊓ q.2
<VAR>α : Type u<VAR>β : Type v<VAR>Sup α<VAR>Sup β<VAR>p q : α × β<GOAL>(p ⊔ q).swap = p.swap ⊔ q.swap
<VAR>α : Type u<VAR>β : Type v<VAR>Inf α<VAR>Inf β<VAR>p q : α × β<GOAL>(p ⊓ q).swap = p.swap ⊓ q.swap
<VAR>α : Type u<VAR>β : Type v<VAR>Sup α<VAR>Sup β<VAR>p q : α × β<GOAL>p ⊔ q = (p.1 ⊔ q.1, p.2 ⊔ q.2)
<VAR>α : Type u<VAR>β : Type v<VAR>Inf α<VAR>Inf β<VAR>p q : α × β<GOAL>p ⊓ q = (p.1 ⊓ q.1, p.2 ⊓ q.2)
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>P : α → Prop<VAR>Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)<VAR>x y : Subtype P<GOAL>↑(x ⊔ y) = ↑x ⊔ ↑y
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>P : α → Prop<VAR>Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)<VAR>x y : Subtype P<GOAL>↑(x ⊓ y) = ↑x ⊓ ↑y
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>P : α → Prop<VAR>Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)<VAR>x y : α<VAR>hx : P x<VAR>hy : P y<GOAL>⟨x, hx⟩ ⊔ ⟨y, hy⟩ = ⟨x ⊔ y, ⋯⟩
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>P : α → Prop<VAR>Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)<VAR>x y : α<VAR>hx : P x<VAR>hy : P y<GOAL>⟨x, hx⟩ ⊓ ⟨y, hy⟩ = ⟨x ⊓ y, ⋯⟩
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : Filter α<GOAL>Filter.IsBounded r f ↔ ∃ s ∈ f.sets, ∃ b, s ⊆ {x | r x b}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>f : Filter β<VAR>u : β → α<GOAL>(∃ b, ∀ (x : β), r (u x) b) → Filter.IsBoundedUnder r f u
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Filter.IsBounded r ⊥ ↔ Nonempty α
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Filter.IsBounded r ⊤ ↔ ∃ t, ∀ (x : α), r x t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>Filter.IsBounded r (𝓟 s) ↔ ∃ t, ∀ x ∈ s, r x t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f g : Filter α<VAR>IsTrans α r<VAR>IsDirected α r<GOAL>Filter.IsBounded r f → Filter.IsBounded r g → Filter.IsBounded r (f ⊔ g)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f g : Filter α<VAR>h : f ≤ g<GOAL>Filter.IsBounded r g → Filter.IsBounded r f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>f g : Filter β<VAR>u : β → α<VAR>h : f ≤ g<GOAL>Filter.IsBoundedUnder r g u → Filter.IsBoundedUnder r f u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>l : Filter α<VAR>u v : α → β<VAR>hu : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l u<VAR>hv : v ≤ᶠ[l] u<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>l : Filter α<VAR>u v : α → β<VAR>hu : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l u<VAR>hv : u ≤ᶠ[l] v<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>l : Filter β<VAR>a : α<GOAL>Filter.IsBoundedUnder r l fun x => a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>f : Filter α<VAR>q : β → β → Prop<VAR>u : α → β<VAR>hu : ∀ (a₀ a₁ : α), r a₀ a₁ → q (u a₀) (u a₁)<GOAL>Filter.IsBounded r f → Filter.IsBoundedUnder q f u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>l : Filter γ<VAR>q : β → β → Prop<VAR>u : γ → α<VAR>v : α → β<VAR>hv : ∀ (a₀ a₁ : α), r a₀ a₁ → q (v a₀) (v a₁)<GOAL>Filter.IsBoundedUnder r l u → Filter.IsBoundedUnder q l (v ∘ u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>f : Filter β<VAR>u : β → α<GOAL>BddAbove (Set.range u) → Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>f : Filter β<VAR>u : β → α<GOAL>BddBelow (Set.range u) → Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>l : Filter γ<VAR>u : γ → α<VAR>v : α → β<VAR>hv : Monotone v<VAR>hl : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l u<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (v ∘ u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>l : Filter γ<VAR>u : γ → α<VAR>v : α → β<VAR>hv : Monotone v<VAR>hl : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l u<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l (v ∘ u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>l : Filter γ<VAR>u : γ → α<VAR>v : α → β<VAR>hv : Antitone v<VAR>hl : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l u<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (v ∘ u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>l : Filter γ<VAR>u : γ → α<VAR>v : α → β<VAR>hv : Antitone v<VAR>hl : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l u<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l (v ∘ u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>NoMaxOrder β<VAR>f : α → β<VAR>l : Filter α<VAR>l.NeBot<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>¬Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>NoMinOrder β<VAR>f : α → β<VAR>l : Filter α<VAR>l.NeBot<VAR>hf : Filter.Tendsto f l Filter.atBot<GOAL>¬Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>IsDirected β fun x x_1 => x ≤ x_1<VAR>f : α → β<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) Filter.cofinite f<GOAL>BddAbove (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>IsDirected β fun x x_1 => x ≥ x_1<VAR>f : α → β<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) Filter.cofinite f<GOAL>BddBelow (Set.range f)
<VAR>β : Type u_2<VAR>Preorder β<VAR>IsDirected β fun x x_1 => x ≤ x_1<VAR>f : ℕ → β<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) Filter.atTop f<GOAL>BddAbove (Set.range f)
<VAR>β : Type u_2<VAR>Preorder β<VAR>IsDirected β fun x x_1 => x ≥ x_1<VAR>f : ℕ → β<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) Filter.atTop f<GOAL>BddBelow (Set.range f)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : Filter α<VAR>IsTrans α r<VAR>a : α<VAR>h : ∀ s ∈ f, ∃ x ∈ s, r a x<GOAL>Filter.IsCobounded r f
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : Filter α<VAR>IsTrans α r<VAR>f.NeBot<GOAL>Filter.IsBounded r f → Filter.IsCobounded (flip r) f
<VAR>α : Type u_1<VAR>f : Filter α<VAR>Preorder α<VAR>f.NeBot<VAR>h : Filter.IsBounded (fun x x_1 => x ≤ x_1) f<GOAL>Filter.IsCobounded (fun x x_1 => x ≥ x_1) f
<VAR>α : Type u_1<VAR>f : Filter α<VAR>Preorder α<VAR>f.NeBot<VAR>h : Filter.IsBounded (fun x x_1 => x ≥ x_1) f<GOAL>Filter.IsCobounded (fun x x_1 => x ≤ x_1) f
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>u : γ → α<VAR>l : Filter γ<VAR>IsTrans α r<VAR>l.NeBot<VAR>h : Filter.IsBoundedUnder r l u<GOAL>Filter.IsCoboundedUnder (flip r) l u
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>u : γ → α<VAR>l : Filter γ<VAR>Preorder α<VAR>l.NeBot<VAR>h : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l u<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) l u
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>u : γ → α<VAR>l : Filter γ<VAR>Preorder α<VAR>l.NeBot<VAR>h : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l u<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) l u
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>Preorder α<VAR>l : Filter ι<VAR>l.NeBot<VAR>f : ι → α<VAR>x : α<VAR>hf : ∀ᶠ (i : ι) in l, x ≤ f i<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) l f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>Preorder α<VAR>l : Filter ι<VAR>l.NeBot<VAR>f : ι → α<VAR>x : α<VAR>hf : ∀ᶠ (i : ι) in l, f i ≤ x<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) l f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>Preorder α<VAR>l : Filter ι<VAR>l.NeBot<VAR>f : ι → α<VAR>x : α<VAR>hf : ∀ (i : ι), x ≤ f i<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) l f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>Preorder α<VAR>l : Filter ι<VAR>l.NeBot<VAR>f : ι → α<VAR>x : α<VAR>hf : ∀ (i : ι), f i ≤ x<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) l f
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Filter.IsCobounded r ⊥ ↔ ∃ b, ∀ (x : α), r b x
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Filter.IsCobounded r ⊤ ↔ Nonempty α
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>Filter.IsCobounded r (𝓟 s) ↔ ∃ b, ∀ (a : α), (∀ x ∈ s, r x a) → r b a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f g : Filter α<VAR>h : f ≤ g<GOAL>Filter.IsCobounded r f → Filter.IsCobounded r g
<VAR>α : Type u_6<VAR>f : Filter α<VAR>R : Type u_7<VAR>Preorder R<VAR>Add R<VAR>CovariantClass R R (fun a b => a + b) fun x x_1 => x ≤ x_1<VAR>CovariantClass R R (fun a b => b + a) fun x x_1 => x ≤ x_1<VAR>u v : α → R<VAR>u_bdd_ge : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u<VAR>v_bdd_ge : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f v<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f (u + v)
<VAR>α : Type u_6<VAR>f : Filter α<VAR>R : Type u_7<VAR>Preorder R<VAR>Add R<VAR>CovariantClass R R (fun a b => a + b) fun x x_1 => x ≤ x_1<VAR>CovariantClass R R (fun a b => b + a) fun x x_1 => x ≤ x_1<VAR>u v : α → R<VAR>u_bdd_le : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u<VAR>v_bdd_le : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f v<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f (u + v)
<VAR>α : Type u_6<VAR>f : Filter α<VAR>R : Type u_7<VAR>κ : Type u_8<VAR>AddCommMonoid R<VAR>r : R → R → Prop<VAR>hr : ∀ (v₁ v₂ : α → R), Filter.IsBoundedUnder r f v₁ → Filter.IsBoundedUnder r f v₂ → Filter.IsBoundedUnder r f (v₁ + v₂)<VAR>hr₀ : r 0 0<VAR>u : κ → α → R<VAR>s : Finset κ<VAR>h : ∀ k ∈ s, Filter.IsBoundedUnder r f (u k)<GOAL>Filter.IsBoundedUnder r f (∑ k ∈ s, u k)
<VAR>α : Type u_6<VAR>f : Filter α<VAR>R : Type u_7<VAR>Preorder R<VAR>κ : Type u_8<VAR>AddCommMonoid R<VAR>CovariantClass R R (fun a b => a + b) fun x x_1 => x ≤ x_1<VAR>CovariantClass R R (fun a b => b + a) fun x x_1 => x ≤ x_1<VAR>u : κ → α → R<VAR>s : Finset κ<GOAL>(∀ k ∈ s, Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f (u k)) → Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f (∑ k ∈ s, u k)
<VAR>α : Type u_6<VAR>f : Filter α<VAR>R : Type u_7<VAR>Preorder R<VAR>κ : Type u_8<VAR>AddCommMonoid R<VAR>CovariantClass R R (fun a b => a + b) fun x x_1 => x ≤ x_1<VAR>CovariantClass R R (fun a b => b + a) fun x x_1 => x ≤ x_1<VAR>u : κ → α → R<VAR>s : Finset κ<GOAL>(∀ k ∈ s, Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f (u k)) → Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f (∑ k ∈ s, u k)
<VAR>α : Type u_1<VAR>Preorder α<VAR>Nonempty α<GOAL>Filter.IsBounded (fun x x_1 => x ≤ x_1) Filter.atBot
<VAR>α : Type u_1<VAR>Preorder α<VAR>Nonempty α<GOAL>Filter.IsBounded (fun x x_1 => x ≥ x_1) Filter.atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Nonempty α<VAR>f : Filter β<VAR>u : β → α<VAR>h : Filter.Tendsto u f Filter.atBot<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Nonempty α<VAR>f : Filter β<VAR>u : β → α<VAR>h : Filter.Tendsto u f Filter.atTop<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u
<VAR>α : Type u_1<VAR>Preorder α<VAR>Nonempty α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>u : ℕ → α<VAR>hx : Filter.Tendsto u Filter.atTop Filter.atBot<GOAL>BddAbove (Set.range u)
<VAR>α : Type u_1<VAR>Preorder α<VAR>Nonempty α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>u : ℕ → α<VAR>hx : Filter.Tendsto u Filter.atTop Filter.atTop<GOAL>BddBelow (Set.range u)
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<VAR>f : Filter α<GOAL>Filter.IsCobounded (fun x x_1 => x ≤ x_1) f
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<VAR>f : Filter α<GOAL>Filter.IsCobounded (fun x x_1 => x ≥ x_1) f
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<VAR>f : Filter α<GOAL>Filter.IsBounded (fun x x_1 => x ≤ x_1) f
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<VAR>f : Filter α<GOAL>Filter.IsBounded (fun x x_1 => x ≥ x_1) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>l : Filter γ<VAR>u : γ → α<GOAL>(Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => e (u x)) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>l : Filter γ<VAR>u : γ → α<GOAL>(Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun x => e (u x)) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedCommGroup α<VAR>l : Filter β<VAR>u : β → α<GOAL>(Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => (u x)⁻¹) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedAddCommGroup α<VAR>l : Filter β<VAR>u : β → α<GOAL>(Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => -u x) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l u