ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a b : ℕ<GOAL>Finset.uIcc a b = { val := ↑(List.range' (min a b) (max a b + 1 - min a b)), nodup := ⋯ }
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Finset.range n = Finset.Icc 0 (n - 1)
<VAR>a b : ℕ<GOAL>(Finset.Icc a b).card = b + 1 - a
<VAR>a b : ℕ<GOAL>(Finset.Ico a b).card = b - a
<VAR>a b : ℕ<GOAL>(Finset.Ioc a b).card = b - a
<VAR>a b : ℕ<GOAL>(Finset.Ioo a b).card = b - a - 1
<VAR>a b : ℕ<GOAL>(Finset.uIcc a b).card = (↑b - ↑a).natAbs + 1
<VAR>b : ℕ<GOAL>(Finset.Iic b).card = b + 1
<VAR>b : ℕ<GOAL>(Finset.Iio b).card = b
<VAR>a b : ℕ<GOAL>Fintype.card ↑(Set.Icc a b) = b + 1 - a
<VAR>a b : ℕ<GOAL>Fintype.card ↑(Set.Ico a b) = b - a
<VAR>a b : ℕ<GOAL>Fintype.card ↑(Set.Ioc a b) = b - a
<VAR>a b : ℕ<GOAL>Fintype.card ↑(Set.Ioo a b) = b - a - 1
<VAR>b : ℕ<GOAL>Fintype.card ↑(Set.Iic b) = b + 1
<VAR>b : ℕ<GOAL>Fintype.card ↑(Set.Iio b) = b
<VAR>a b : ℕ<GOAL>Finset.Icc a.succ b = Finset.Ioc a b
<VAR>a b : ℕ<GOAL>Finset.Ico a b.succ = Finset.Icc a b
<VAR>a b : ℕ<GOAL>Finset.Ico a.succ b = Finset.Ioo a b
<VAR>a : ℕ<VAR>b : ℕ<VAR>h : 0 < b<GOAL>Finset.Icc a (b - 1) = Finset.Ico a b
<VAR>a b : ℕ<GOAL>Finset.Ico a.succ b.succ = Finset.Ioc a b
<VAR>a : ℕ<GOAL>Finset.Ico a (a + 1) = {a}
<VAR>a : ℕ<VAR>h : 0 < a<GOAL>Finset.Ico (a - 1) a = {a - 1}
<VAR>b : ℕ<GOAL>Finset.Ioc b (b + 1) = {b + 1}
<VAR>a b : ℕ<VAR>h : a ≤ b<GOAL>Finset.Ico a (b + 1) = insert b (Finset.Ico a b)
<VAR>a b : ℕ<VAR>h : a < b<GOAL>insert a (Finset.Ico a.succ b) = Finset.Ico a b
<VAR>a b : ℕ<VAR>h : a ≤ b<GOAL>insert a (Finset.Icc (a + 1) b) = Finset.Icc a b
<VAR>a b : ℕ<VAR>h : a ≤ b + 1<GOAL>insert (b + 1) (Finset.Icc a b) = Finset.Icc a (b + 1)
<VAR>a b c : ℕ<VAR>h : c ≤ a<GOAL>Finset.image (fun x => x - c) (Finset.Ico a b) = Finset.Ico (a - c) (b - c)
<VAR>a b c : ℕ<VAR>hac : a ≤ c<GOAL>Finset.image (fun x => c - x) (Finset.Ico a b) = Finset.Ico (c + 1 - b) (c + 1 - a)
<VAR>a b : ℕ<GOAL>Finset.Ico a.succ b = (Finset.Ico a b).erase a
<VAR>n a : ℕ<GOAL>Set.InjOn (fun x => x % a) ↑(Finset.Ico n (n + a))
<VAR>n a : ℕ<GOAL>Finset.image (fun x => x % a) (Finset.Ico n (n + a)) = Finset.range a
<VAR>n a : ℕ<GOAL>Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = Multiset.range a
<VAR>n : ℕ<GOAL>Finset.image (fun j => n - 1 - j) (Finset.range n) = Finset.range n
<VAR>a b : ℕ<GOAL>Finset.range (a + b) = Finset.range a ∪ Finset.map (addLeftEmbedding a) (Finset.range b)
<VAR>P : ℕ → Prop<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>hP : ¬BddAbove {x | P x}<VAR>n : ℕ<GOAL>P n
<VAR>P : ℕ → Prop<VAR>base : ∃ n, ∀ m > n, P m<VAR>step : ∀ (n : ℕ), (∀ m > n, P m) → P n<VAR>n : ℕ<GOAL>P n
<VAR>P : ℕ → Prop<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>hP : {x | P x}.Infinite<VAR>n : ℕ<GOAL>P n
<VAR>P : ℕ → Prop<VAR>seed : ℕ<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>hs : P seed<VAR>hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y<VAR>n : ℕ<GOAL>P n
<VAR>P : ℕ → Prop<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>seed : ℕ<VAR>hs : P seed<VAR>f : ℕ → ℕ<VAR>hf : ∀ (x : ℕ), seed ≤ x → P x → x < f x ∧ P (f x)<VAR>n : ℕ<GOAL>P n
<VAR>P : ℕ → Prop<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>k seed : ℕ<VAR>hk : 1 < k<VAR>hs : P seed.succ<VAR>hm : ∀ (x : ℕ), seed < x → P x → P (k * x)<VAR>n : ℕ<GOAL>P n
<VAR>P : ℕ → Prop<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>seed : ℕ<VAR>hs : P seed.succ<VAR>hm : ∀ (x : ℕ), seed < x → P x → P (2 * x)<VAR>n : ℕ<GOAL>P n
<VAR>M : Type u_1<VAR>Monoid M<VAR>k : ℕ<VAR>hk : 1 < k<VAR>P : M → Prop<VAR>hmul : ∀ (x y : M), P x → P (x * y) ∨ P (y * x)<VAR>hpow : ∀ (x : M), P (x ^ k) → P x<VAR>n : ℕ<VAR>x : M<GOAL>P (x ^ n) → P x
<VAR>α : Type u_1<VAR>self : CircularPreorder α<VAR>a b c : α<GOAL>btw a b c → btw b c a
<VAR>α : Type u_1<VAR>self : CircularPreorder α<VAR>a b c : α<GOAL>sbtw a b c ↔ btw a b c ∧ ¬btw c b a
<VAR>α : Type u_1<VAR>self : CircularPreorder α<VAR>a : α<GOAL>btw a a a
<VAR>α : Type u_1<VAR>self : CircularPreorder α<VAR>a b c d : α<GOAL>sbtw a b c → sbtw b d c → sbtw a d c
<VAR>α : Type u_1<VAR>self : CircularPartialOrder α<VAR>a b c : α<GOAL>btw a b c → btw c b a → a = b ∨ b = c ∨ c = a
<VAR>α : Type u_1<VAR>self : CircularOrder α<VAR>a b c : α<GOAL>btw a b c ∨ btw c b a
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a : α<GOAL>btw a a a
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c : α<VAR>h : btw a b c<GOAL>btw b c a
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c : α<VAR>h : btw a b c<GOAL>btw c a b
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c : α<GOAL>btw a b c ↔ btw c a b
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c : α<GOAL>sbtw a b c ↔ btw a b c ∧ ¬btw c b a
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c : α<VAR>h : sbtw a b c<GOAL>btw a b c
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c : α<VAR>h : sbtw a b c<GOAL>¬btw c b a
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c : α<VAR>h : btw a b c<GOAL>¬sbtw c b a
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c : α<VAR>habc : btw a b c<VAR>hcba : ¬btw c b a<GOAL>sbtw a b c
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c : α<VAR>h : sbtw a b c<GOAL>sbtw b c a
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c : α<VAR>h : sbtw a b c<GOAL>sbtw c a b
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c : α<GOAL>sbtw a b c ↔ sbtw c a b
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c d : α<VAR>h : sbtw a b c<GOAL>sbtw b d c → sbtw a d c
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c d : α<VAR>hbc : sbtw a b c<VAR>hcd : sbtw a c d<GOAL>sbtw a b d
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b c : α<VAR>h : sbtw a b c<GOAL>¬sbtw c b a
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b : α<GOAL>¬sbtw a b a
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b : α<GOAL>¬sbtw a a b
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b : α<GOAL>¬sbtw a b b
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a : α<GOAL>¬sbtw a a a
<VAR>α : Type u_1<VAR>CircularPartialOrder α<VAR>a b c : α<VAR>h : btw a b c<GOAL>btw c b a → a = b ∨ b = c ∨ c = a
<VAR>α : Type u_1<VAR>CircularOrder α<VAR>a b : α<GOAL>btw a b a
<VAR>α : Type u_1<VAR>CircularOrder α<VAR>a b : α<GOAL>btw a a b
<VAR>α : Type u_1<VAR>CircularOrder α<VAR>a b : α<GOAL>btw a b b
<VAR>α : Type u_1<VAR>CircularOrder α<VAR>a b c : α<GOAL>sbtw a b c ↔ ¬btw c b a
<VAR>α : Type u_1<VAR>CircularOrder α<VAR>a b c : α<GOAL>btw a b c ↔ ¬sbtw c b a
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b x : α<GOAL>x ∈ Set.cIcc a b ↔ btw a x b
<VAR>α : Type u_1<VAR>CircularPreorder α<VAR>a b x : α<GOAL>x ∈ Set.cIoo a b ↔ sbtw a x b
<VAR>α : Type u_1<VAR>CircularOrder α<VAR>a b : α<GOAL>a ∈ Set.cIcc a b
<VAR>α : Type u_1<VAR>CircularOrder α<VAR>a b : α<GOAL>b ∈ Set.cIcc a b
<VAR>α : Type u_1<VAR>CircularOrder α<VAR>a b : α<GOAL>(Set.cIcc a b)ᶜ = Set.cIoo b a
<VAR>α : Type u_1<VAR>CircularOrder α<VAR>a b : α<GOAL>(Set.cIoo a b)ᶜ = Set.cIcc b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>h : MonotoneOn f s<VAR>hl : BddBelow (f '' s)<VAR>hu : BddAbove (f '' s)<GOAL>∃ g, Monotone g ∧ Set.EqOn f g s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>h : AntitoneOn f s<VAR>hl : BddBelow (f '' s)<VAR>hu : BddAbove (f '' s)<GOAL>∃ g, Antitone g ∧ Set.EqOn f g s
<VAR>α : Type u_1<VAR>ι : Type u_9<VAR>SupSet α<VAR>f : ULift.{u_10, u_9} ι → α<GOAL>⨆ i, f i = ⨆ i, f { down := i }
<VAR>α : Type u_1<VAR>ι : Type u_9<VAR>InfSet α<VAR>f : ULift.{u_10, u_9} ι → α<GOAL>⨅ i, f i = ⨅ i, f { down := i }
<VAR>α : Type u_9<VAR>self : CompleteSemilatticeSup α<VAR>s : Set α<VAR>a : α<GOAL>a ∈ s → a ≤ sSup s
<VAR>α : Type u_9<VAR>self : CompleteSemilatticeSup α<VAR>s : Set α<VAR>a : α<GOAL>(∀ b ∈ s, b ≤ a) → sSup s ≤ a
<VAR>α : Type u_1<VAR>CompleteSemilatticeSup α<VAR>s : Set α<VAR>a : α<GOAL>a ∈ s → a ≤ sSup s
<VAR>α : Type u_1<VAR>CompleteSemilatticeSup α<VAR>s : Set α<VAR>a : α<GOAL>(∀ b ∈ s, b ≤ a) → sSup s ≤ a
<VAR>α : Type u_1<VAR>CompleteSemilatticeSup α<VAR>s : Set α<GOAL>IsLUB s (sSup s)
<VAR>α : Type u_1<VAR>CompleteSemilatticeSup α<VAR>s : Set α<VAR>a : α<GOAL>IsLUB s a ↔ sSup s = a
<VAR>α : Type u_1<VAR>CompleteSemilatticeSup α<VAR>s : Set α<VAR>a b : α<VAR>hb : b ∈ s<VAR>h : a ≤ b<GOAL>a ≤ sSup s
<VAR>α : Type u_1<VAR>CompleteSemilatticeSup α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>sSup s ≤ sSup t
<VAR>α : Type u_1<VAR>CompleteSemilatticeSup α<VAR>s : Set α<VAR>a : α<GOAL>sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a
<VAR>α : Type u_1<VAR>CompleteSemilatticeSup α<VAR>s : Set α<VAR>a : α<GOAL>a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteSemilatticeSup α<VAR>a : α<VAR>s : ι → α<GOAL>a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b
<VAR>α : Type u_1<VAR>CompleteSemilatticeSup α<VAR>s t : Set α<VAR>h : ∀ x ∈ s, ∃ y ∈ t, x ≤ y<GOAL>sSup s ≤ sSup t
<VAR>α : Type u_1<VAR>CompleteSemilatticeSup α<VAR>a : α<GOAL>sSup {a} = a
<VAR>α : Type u_9<VAR>self : CompleteSemilatticeInf α<VAR>s : Set α<VAR>a : α<GOAL>(∀ b ∈ s, a ≤ b) → a ≤ sInf s
<VAR>α : Type u_9<VAR>self : CompleteSemilatticeInf α<VAR>s : Set α<VAR>a : α<GOAL>a ∈ s → sInf s ≤ a
<VAR>α : Type u_1<VAR>CompleteSemilatticeInf α<VAR>s : Set α<VAR>a : α<GOAL>a ∈ s → sInf s ≤ a
<VAR>α : Type u_1<VAR>CompleteSemilatticeInf α<VAR>s : Set α<VAR>a : α<GOAL>(∀ b ∈ s, a ≤ b) → a ≤ sInf s
<VAR>α : Type u_1<VAR>CompleteSemilatticeInf α<VAR>s : Set α<GOAL>IsGLB s (sInf s)
<VAR>α : Type u_1<VAR>CompleteSemilatticeInf α<VAR>s : Set α<VAR>a : α<GOAL>IsGLB s a ↔ sInf s = a
<VAR>α : Type u_1<VAR>CompleteSemilatticeInf α<VAR>s : Set α<VAR>a b : α<VAR>hb : b ∈ s<VAR>h : b ≤ a<GOAL>sInf s ≤ a
<VAR>α : Type u_1<VAR>CompleteSemilatticeInf α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>sInf t ≤ sInf s
<VAR>α : Type u_1<VAR>CompleteSemilatticeInf α<VAR>s : Set α<VAR>a : α<GOAL>a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b
<VAR>α : Type u_1<VAR>CompleteSemilatticeInf α<VAR>s : Set α<VAR>a : α<GOAL>sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteSemilatticeInf α<VAR>a : α<VAR>s : ι → α<GOAL>iInf s ≤ a ↔ ∀ (b : α), (∀ (i : ι), b ≤ s i) → b ≤ a
<VAR>α : Type u_1<VAR>CompleteSemilatticeInf α<VAR>s t : Set α<VAR>h : ∀ x ∈ s, ∃ y ∈ t, y ≤ x<GOAL>sInf t ≤ sInf s
<VAR>α : Type u_1<VAR>CompleteSemilatticeInf α<VAR>a : α<GOAL>sInf {a} = a
<VAR>α : Type u_9<VAR>self : CompleteLattice α<VAR>x : α<GOAL>x ≤ ⊤
<VAR>α : Type u_9<VAR>self : CompleteLattice α<VAR>x : α<GOAL>⊥ ≤ x
<VAR>α : Type u_9<VAR>self : CompleteLinearOrder α<VAR>a b : α<GOAL>a ≤ b ∨ b ≤ a
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>OrderDual.toDual (sSup s) = sInf (⇑OrderDual.ofDual ⁻¹' s)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>OrderDual.toDual (sInf s) = sSup (⇑OrderDual.ofDual ⁻¹' s)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set αᵒᵈ<GOAL>OrderDual.ofDual (sSup s) = sInf (⇑OrderDual.toDual ⁻¹' s)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set αᵒᵈ<GOAL>OrderDual.ofDual (sInf s) = sSup (⇑OrderDual.toDual ⁻¹' s)
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<GOAL>OrderDual.toDual (⨆ i, f i) = ⨅ i, OrderDual.toDual (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<GOAL>OrderDual.toDual (⨅ i, f i) = ⨆ i, OrderDual.toDual (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → αᵒᵈ<GOAL>OrderDual.ofDual (⨆ i, f i) = ⨅ i, OrderDual.ofDual (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → αᵒᵈ<GOAL>OrderDual.ofDual (⨅ i, f i) = ⨆ i, OrderDual.ofDual (f i)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>sInf s ≤ sSup s
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s t : Set α<GOAL>sSup (s ∪ t) = sSup s ⊔ sSup t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s t : Set α<GOAL>sInf (s ∪ t) = sInf s ⊓ sInf t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s t : Set α<GOAL>sSup (s ∩ t) ≤ sSup s ⊓ sSup t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s t : Set α<GOAL>sInf s ⊔ sInf t ≤ sInf (s ∩ t)
<VAR>α : Type u_1<VAR>CompleteLattice α<GOAL>sSup ∅ = ⊥
<VAR>α : Type u_1<VAR>CompleteLattice α<GOAL>sInf ∅ = ⊤
<VAR>α : Type u_1<VAR>CompleteLattice α<GOAL>sSup Set.univ = ⊤
<VAR>α : Type u_1<VAR>CompleteLattice α<GOAL>sInf Set.univ = ⊥
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a : α<VAR>s : Set α<GOAL>sSup (insert a s) = a ⊔ sSup s
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a : α<VAR>s : Set α<GOAL>sInf (insert a s) = a ⊓ sInf s
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s t : Set α<VAR>h : s ⊆ insert ⊥ t<GOAL>sSup s ≤ sSup t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s t : Set α<VAR>h : s ⊆ insert ⊤ t<GOAL>sInf t ≤ sInf s
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>sSup (s \ {⊥}) = sSup s
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>sInf (s \ {⊤}) = sInf s
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a b : α<GOAL>sSup {a, b} = a ⊔ b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a b : α<GOAL>sInf {a, b} = a ⊓ b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>sSup s = ⊥ ↔ ∀ a ∈ s, a = ⊥
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>sInf s = ⊤ ↔ ∀ a ∈ s, a = ⊤
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥}
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<VAR>h_sup : sSup s = ⊥<VAR>hne : s.Nonempty<GOAL>s = {⊥}
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>sInf s = ⊤ → s.Nonempty → s = {⊤}
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<VAR>b : α<VAR>h₁ : ∀ a ∈ s, a ≤ b<VAR>h₂ : ∀ w < b, ∃ a ∈ s, w < a<GOAL>sSup s = b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<VAR>b : α<GOAL>(∀ a ∈ s, b ≤ a) → (∀ (w : α), b < w → ∃ a ∈ s, a < w) → sInf s = b
<VAR>α : Type u_1<VAR>CompleteLinearOrder α<VAR>s : Set α<VAR>b : α<GOAL>b < sSup s ↔ ∃ a ∈ s, b < a
<VAR>α : Type u_1<VAR>CompleteLinearOrder α<VAR>s : Set α<VAR>b : α<GOAL>sInf s < b ↔ ∃ a ∈ s, a < b
<VAR>α : Type u_1<VAR>CompleteLinearOrder α<VAR>s : Set α<GOAL>sSup s = ⊤ ↔ ∀ b < ⊤, ∃ a ∈ s, b < a
<VAR>α : Type u_1<VAR>CompleteLinearOrder α<VAR>s : Set α<GOAL>sInf s = ⊥ ↔ ∀ b > ⊥, ∃ a ∈ s, a < b
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLinearOrder α<VAR>a : α<VAR>f : ι → α<GOAL>a < iSup f ↔ ∃ i, a < f i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLinearOrder α<VAR>a : α<VAR>f : ι → α<GOAL>iInf f < a ↔ ∃ i, f i < a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>SupSet α<VAR>f : ι → α<GOAL>sSup (Set.range f) = iSup f
<VAR>α : Type u_1<VAR>SupSet α<VAR>s : Set α<GOAL>sSup s = ⨆ a, ↑a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>SupSet α<VAR>f g : ι → α<VAR>h : ∀ (i : ι), f i = g i<GOAL>⨆ i, f i = ⨆ i, g i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>SupSet α<VAR>f g : ι → α<VAR>p : ι → Prop<VAR>h : ∀ (i : ι), p i → f i = g i<GOAL>⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), g i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>SupSet α<VAR>p : ι → Prop<VAR>f g : (i : ι) → p i → α<VAR>h : ∀ (i : ι) (hi : p i), f i hi = g i hi<GOAL>⨆ i, ⨆ (hi : p i), f i hi = ⨆ i, ⨆ (hi : p i), g i hi
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>SupSet α<VAR>f : ι → ι'<VAR>hf : Function.Surjective f<VAR>g : ι' → α<GOAL>⨆ x, g (f x) = ⨆ y, g y
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>SupSet α<VAR>g : ι' → α<VAR>e : ι ≃ ι'<GOAL>⨆ x, g (e x) = ⨆ y, g y
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>SupSet α<VAR>f : ι → α<VAR>g : ι' → α<VAR>h : ι → ι'<VAR>h1 : Function.Surjective h<VAR>h2 : ∀ (x : ι), g (h x) = f x<GOAL>⨆ x, f x = ⨆ y, g y
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>SupSet α<VAR>f : ι → α<VAR>g : ι' → α<VAR>e : ι ≃ ι'<VAR>h : ∀ (x : ι), g (e x) = f x<GOAL>⨆ x, f x = ⨆ y, g y
<VAR>α : Type u_1<VAR>SupSet α<VAR>p q : Prop<VAR>f₁ : p → α<VAR>f₂ : q → α<VAR>pq : p ↔ q<VAR>f : ∀ (x : q), f₁ ⋯ = f₂ x<GOAL>iSup f₁ = iSup f₂
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>SupSet α<VAR>f : PLift ι → α<GOAL>⨆ i, f { down := i } = ⨆ i, f i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>SupSet α<VAR>f : ι → α<GOAL>⨆ i, f i.down = ⨆ i, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>SupSet α<VAR>g : β → α<VAR>f : ι → β<GOAL>⨆ b, g ↑b = ⨆ i, g (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SupSet α<VAR>s : Set β<VAR>f : β → α<GOAL>sSup (f '' s) = ⨆ a, f ↑a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>InfSet α<VAR>f : ι → α<GOAL>sInf (Set.range f) = iInf f
<VAR>α : Type u_1<VAR>InfSet α<VAR>s : Set α<GOAL>sInf s = ⨅ a, ↑a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>InfSet α<VAR>f g : ι → α<VAR>h : ∀ (i : ι), f i = g i<GOAL>⨅ i, f i = ⨅ i, g i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>InfSet α<VAR>f g : ι → α<VAR>p : ι → Prop<VAR>h : ∀ (i : ι), p i → f i = g i<GOAL>⨅ i, ⨅ (_ : p i), f i = ⨅ i, ⨅ (_ : p i), g i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>InfSet α<VAR>p : ι → Prop<VAR>f g : (i : ι) → p i → α<VAR>h : ∀ (i : ι) (hi : p i), f i hi = g i hi<GOAL>⨅ i, ⨅ (hi : p i), f i hi = ⨅ i, ⨅ (hi : p i), g i hi
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>InfSet α<VAR>f : ι → ι'<VAR>hf : Function.Surjective f<VAR>g : ι' → α<GOAL>⨅ x, g (f x) = ⨅ y, g y
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>InfSet α<VAR>g : ι' → α<VAR>e : ι ≃ ι'<GOAL>⨅ x, g (e x) = ⨅ y, g y
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>InfSet α<VAR>f : ι → α<VAR>g : ι' → α<VAR>h : ι → ι'<VAR>h1 : Function.Surjective h<VAR>h2 : ∀ (x : ι), g (h x) = f x<GOAL>⨅ x, f x = ⨅ y, g y
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>InfSet α<VAR>f : ι → α<VAR>g : ι' → α<VAR>e : ι ≃ ι'<VAR>h : ∀ (x : ι), g (e x) = f x<GOAL>⨅ x, f x = ⨅ y, g y
<VAR>α : Type u_1<VAR>InfSet α<VAR>p q : Prop<VAR>f₁ : p → α<VAR>f₂ : q → α<VAR>pq : p ↔ q<VAR>f : ∀ (x : q), f₁ ⋯ = f₂ x<GOAL>iInf f₁ = iInf f₂
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>InfSet α<VAR>f : PLift ι → α<GOAL>⨅ i, f { down := i } = ⨅ i, f i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>InfSet α<VAR>f : ι → α<GOAL>⨅ i, f i.down = ⨅ i, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>InfSet α<VAR>g : β → α<VAR>f : ι → β<GOAL>⨅ b, g ↑b = ⨅ i, g (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>InfSet α<VAR>s : Set β<VAR>f : β → α<GOAL>sInf (f '' s) = ⨅ a, f ↑a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>i : ι<GOAL>f i ≤ iSup f
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>i : ι<GOAL>iInf f ≤ f i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<GOAL>IsLUB (Set.range f) (⨆ j, f j)
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<GOAL>IsGLB (Set.range f) (⨅ j, f j)
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>a : α<VAR>h : IsLUB (Set.range f) a<GOAL>⨆ j, f j = a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>a : α<VAR>h : IsGLB (Set.range f) a<GOAL>⨅ j, f j = a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>a : α<VAR>i : ι<VAR>h : a ≤ f i<GOAL>a ≤ iSup f
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>a : α<VAR>i : ι<VAR>h : f i ≤ a<GOAL>iInf f ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>f : (i : ι) → κ i → α<VAR>i : ι<VAR>j : κ i<GOAL>f i j ≤ ⨆ i, ⨆ j, f i j
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>f : (i : ι) → κ i → α<VAR>i : ι<VAR>j : κ i<GOAL>⨅ i, ⨅ j, f i j ≤ f i j
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>a : α<VAR>f : (i : ι) → κ i → α<VAR>i : ι<VAR>j : κ i<VAR>h : a ≤ f i j<GOAL>a ≤ ⨆ i, ⨆ j, f i j
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>a : α<VAR>f : (i : ι) → κ i → α<VAR>i : ι<VAR>j : κ i<VAR>h : f i j ≤ a<GOAL>⨅ i, ⨅ j, f i j ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>a : α<VAR>h : ∀ (i : ι), f i ≤ a<GOAL>iSup f ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>a : α<VAR>h : ∀ (i : ι), a ≤ f i<GOAL>a ≤ iInf f
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>a : α<VAR>f : (i : ι) → κ i → α<VAR>h : ∀ (i : ι) (j : κ i), f i j ≤ a<GOAL>⨆ i, ⨆ j, f i j ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>a : α<VAR>f : (i : ι) → κ i → α<VAR>h : ∀ (i : ι) (j : κ i), a ≤ f i j<GOAL>a ≤ ⨅ i, ⨅ j, f i j
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>κ : ι → Sort u_9<VAR>f : ι → α<GOAL>⨆ i, ⨆ x, f i ≤ ⨆ i, f i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>κ : ι → Sort u_9<VAR>f : ι → α<GOAL>⨅ i, f i ≤ ⨅ i, ⨅ x, f i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f g : ι → α<VAR>h : ∀ (i : ι), f i ≤ g i<GOAL>iSup f ≤ iSup g
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f g : ι → α<VAR>h : ∀ (i : ι), f i ≤ g i<GOAL>iInf f ≤ iInf g
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>f g : (i : ι) → κ i → α<VAR>h : ∀ (i : ι) (j : κ i), f i j ≤ g i j<GOAL>⨆ i, ⨆ j, f i j ≤ ⨆ i, ⨆ j, g i j
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>f g : (i : ι) → κ i → α<VAR>h : ∀ (i : ι) (j : κ i), f i j ≤ g i j<GOAL>⨅ i, ⨅ j, f i j ≤ ⨅ i, ⨅ j, g i j
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>CompleteLattice α<VAR>f : ι → α<VAR>g : ι' → α<VAR>h : ∀ (i : ι), ∃ i', f i ≤ g i'<GOAL>iSup f ≤ iSup g
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>CompleteLattice α<VAR>f : ι → α<VAR>g : ι' → α<VAR>h : ∀ (i' : ι'), ∃ i, f i ≤ g i'<GOAL>iInf f ≤ iInf g
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>CompleteLattice α<VAR>f : (i : ι) → κ i → α<VAR>g : (i' : ι') → κ' i' → α<VAR>h : ∀ (i : ι) (j : κ i), ∃ i' j', f i j ≤ g i' j'<GOAL>⨆ i, ⨆ j, f i j ≤ ⨆ i, ⨆ j, g i j
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>CompleteLattice α<VAR>f : (i : ι) → κ i → α<VAR>g : (i' : ι') → κ' i' → α<VAR>h : ∀ (i : ι') (j : κ' i), ∃ i' j', f i' j' ≤ g i j<GOAL>⨅ i, ⨅ j, f i j ≤ ⨅ i, ⨅ j, g i j
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>CompleteLattice α<VAR>a : α<VAR>h : ι → ι'<GOAL>⨆ x, a ≤ ⨆ x, a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>CompleteLattice α<VAR>a : α<VAR>h : ι' → ι<GOAL>⨅ x, a ≤ ⨅ x, a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>CompleteLattice α<VAR>f : ι → ι' → α<GOAL>⨆ i, ⨅ j, f i j ≤ ⨅ j, ⨆ i, f i j
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>p q : ι → Prop<VAR>hpq : ∀ (i : ι), p i → q i<GOAL>⨆ i, ⨆ (_ : p i), f i ≤ ⨆ i, ⨆ (_ : q i), f i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>p q : ι → Prop<VAR>hpq : ∀ (i : ι), p i → q i<GOAL>⨅ i, ⨅ (_ : q i), f i ≤ ⨅ i, ⨅ (_ : p i), f i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>a : α<GOAL>iSup f ≤ a ↔ ∀ (i : ι), f i ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>a : α<GOAL>a ≤ iInf f ↔ ∀ (i : ι), a ≤ f i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>a : α<VAR>f : (i : ι) → κ i → α<GOAL>⨆ i, ⨆ j, f i j ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>a : α<VAR>f : (i : ι) → κ i → α<GOAL>a ≤ ⨅ i, ⨅ j, f i j ↔ ∀ (i : ι) (j : κ i), a ≤ f i j
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>a : α<GOAL>iSup f < a ↔ ∃ b < a, ∀ (i : ι), f i ≤ b
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>a : α<GOAL>a < iInf f ↔ ∃ b, a < b ∧ ∀ (i : ι), b ≤ f i
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>sSup s = ⨆ a ∈ s, a
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>sInf s = ⨅ a ∈ s, a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>s : ι → α<VAR>CompleteLattice β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>⨆ i, f (s i) ≤ f (iSup s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>s : ι → α<VAR>CompleteLattice β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>⨆ i, f (s i) ≤ f (iInf s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α → β<VAR>hf : Monotone f<VAR>s : (i : ι) → κ i → α<GOAL>⨆ i, ⨆ j, f (s i j) ≤ f (⨆ i, ⨆ j, s i j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α → β<VAR>hf : Antitone f<VAR>s : (i : ι) → κ i → α<GOAL>⨆ i, ⨆ j, f (s i j) ≤ f (⨅ i, ⨅ j, s i j)