ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>p : Prop<VAR>Decidable p<VAR>f : p → α<GOAL>⨆ (h : p), f h = if h : p then f h else sSup ∅
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>p : Prop<VAR>Decidable p<VAR>f : p → α<GOAL>⨅ (h : p), f h = if h : p then f h else sInf ∅
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>p : ι → Prop<VAR>f : Subtype p → α<VAR>hp : ∀ (i : ι), p i<GOAL>⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>p : ι → Prop<VAR>f : Subtype p → α<VAR>hp : ∀ (i : ι), p i<GOAL>⨅ i, ⨅ (h : p i), f ⟨i, h⟩ = iInf f
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>b : α<VAR>Nonempty ι<VAR>f : ι → α<VAR>h₁ : ∀ (i : ι), f i ≤ b<VAR>h₂ : ∀ w < b, ∃ i, w < f i<GOAL>⨆ i, f i = b
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>b : α<VAR>Nonempty ι<VAR>f : ι → α<VAR>h₁ : ∀ (i : ι), b ≤ f i<VAR>h₂ : ∀ (w : α), b < w → ∃ i, f i < w<GOAL>⨅ i, f i = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>SemilatticeSup β<VAR>f g : β → α<VAR>hf : Monotone f<VAR>hg : Antitone g<VAR>h : f ≤ g<GOAL>⨆ n, f n ∈ ⋂ n, Set.Icc (f n) (g n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>SemilatticeSup β<VAR>f g : β → α<VAR>h : Antitone fun n => Set.Icc (f n) (g n)<VAR>h' : ∀ (n : β), f n ≤ g n<GOAL>⨆ n, f n ∈ ⋂ n, Set.Icc (f n) (g n)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>b : α<VAR>hs : s.Nonempty<VAR>h_is_ub : ∀ a ∈ s, a ≤ b<VAR>h_b_le_ub : ∀ (ub : α), (∀ a ∈ s, a ≤ ub) → b ≤ ub<GOAL>sSup s = b
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>Nonempty ι<VAR>f : ι → α<VAR>hf : BddBelow (Set.range f)<GOAL>Set.Iic (⨅ i, f i) = ⋂ i, Set.Iic (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>Nonempty ι<VAR>f : ι → α<VAR>hf : BddAbove (Set.range f)<GOAL>Set.Ici (⨆ i, f i) = ⋂ i, Set.Ici (f i)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>OrderTop α<VAR>h : ⊤ ∈ s<GOAL>sSup s = ⊤
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>OrderBot α<VAR>h : ⊥ ∈ s<GOAL>sInf s = ⊥
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>b : α<VAR>hs : s.Nonempty<VAR>hb : b < sSup s<GOAL>∃ a ∈ s, b < a
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrder α<VAR>b : α<VAR>Nonempty ι<VAR>f : ι → α<VAR>h : b < iSup f<GOAL>∃ i, b < f i
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>b : α<VAR>hs : s.Nonempty<VAR>hb : sInf s < b<GOAL>∃ a ∈ s, a < b
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrder α<VAR>a : α<VAR>Nonempty ι<VAR>f : ι → α<VAR>h : iInf f < a<GOAL>∃ i, f i < a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hs : ¬BddAbove s<GOAL>sSup s = sSup ∅
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hs : ¬BddAbove s<GOAL>sSup s = sSup Set.univ
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hs : ¬BddBelow s<GOAL>sInf s = sInf ∅
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hs : ¬BddBelow s<GOAL>sInf s = sInf Set.univ
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s t : Set α<VAR>hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y<VAR>ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x<GOAL>sSup s = sSup t
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s t : Set α<VAR>hs : ∀ x ∈ s, ∃ y ∈ t, y ≤ x<VAR>ht : ∀ y ∈ t, ∃ x ∈ s, x ≤ y<GOAL>sInf s = sInf t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrder α<VAR>f : ι → α<GOAL>sSup (⋃ i, Set.Iic (f i)) = ⨆ i, f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrder α<VAR>f : ι → α<GOAL>sInf (⋃ i, Set.Ici (f i)) = ⨅ i, f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrder α<VAR>p : ι → Prop<VAR>f : Subtype p → α<VAR>hp : ¬∀ (i : ι), p i<GOAL>⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f ⊔ sSup ∅
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrder α<VAR>p : ι → Prop<VAR>f : Subtype p → α<VAR>hp : ¬∀ (i : ι), p i<GOAL>⨅ i, ⨅ (h : p i), f ⟨i, h⟩ = iInf f ⊓ sInf ∅
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>hs : s.Nonempty<GOAL>sInf s = Function.argminOn id ⋯ s hs
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>hs : s.Nonempty<GOAL>IsLeast s (sInf s)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>b : α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>hs : s.Nonempty<GOAL>b ≤ sInf s ↔ b ∈ lowerBounds s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>hs : s.Nonempty<GOAL>sInf s ∈ s
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrder α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>Nonempty ι<VAR>f : ι → α<GOAL>iInf f ∈ Set.range f
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>β : Type u_5<VAR>ConditionallyCompleteLattice β<VAR>f : α → β<VAR>hf : MonotoneOn f s<VAR>hs : s.Nonempty<GOAL>f (sInf s) = sInf (f '' s)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>β : Type u_5<VAR>ConditionallyCompleteLattice β<VAR>f : α → β<VAR>hf : Monotone f<VAR>hs : s.Nonempty<GOAL>f (sInf s) = sInf (f '' s)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderBot α<GOAL>sInf Set.univ = ⊥
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<GOAL>sSup ∅ = ⊥
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrderBot α<VAR>IsEmpty ι<VAR>f : ι → α<GOAL>⨆ i, f i = ⊥
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<VAR>f : False → α<GOAL>⨆ (i : False), f i = ⊥
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>hs : BddAbove s<GOAL>IsLUB s (sSup s)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>hs : BddAbove s<VAR>a : α<GOAL>sSup s ≤ a ↔ ∀ x ∈ s, x ≤ a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ upperBounds s<GOAL>sSup s ≤ a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>a : α<VAR>h : BddAbove s<GOAL>a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : ι → α<VAR>a : α<VAR>h : BddAbove (Set.range s)<GOAL>a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>a : α<VAR>ne : s.Nonempty<GOAL>a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrderBot α<VAR>Nonempty ι<VAR>f : ι → α<VAR>a : α<GOAL>a ≤ iInf f ↔ ∀ (i : ι), a ≤ f i
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<GOAL>sInf s ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<VAR>i : ι<GOAL>iInf f ≤ f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<VAR>a : α<VAR>c : ι<GOAL>f c ≤ a → iInf f ≤ a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>a : α<VAR>h : a < sSup s<GOAL>∃ b ∈ s, a < b
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<VAR>h : BddAbove (Set.range f)<VAR>a : α<GOAL>⨆ i, f i ≤ a ↔ ∀ (i : ι), f i ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<VAR>a : α<VAR>h : ∀ (i : ι), f i ≤ a<GOAL>⨆ i, f i ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<VAR>a : α<VAR>h : a < ⨆ i, f i<GOAL>∃ i, a < f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrderBot α<VAR>ι' : Sort u_5<VAR>f : ι → α<VAR>g : ι' → α<VAR>hg : BddAbove (Set.range g)<VAR>h : ∀ (i : ι), ∃ i', f i ≤ g i'<GOAL>iSup f ≤ iSup g
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s t : Set α<VAR>h₁ : t.Nonempty<VAR>h₂ : t ⊆ s<GOAL>sInf s ≤ sInf t
<VAR>β : Type u_5<VAR>ConditionallyCompleteLattice β<VAR>s : Set (WithTop β)<VAR>hs : s.Nonempty<GOAL>IsLUB s (sSup s)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : Set (WithTop α)<GOAL>IsLUB s (sSup s)
<VAR>β : Type u_5<VAR>ConditionallyCompleteLattice β<VAR>s : Set (WithTop β)<VAR>hs : BddBelow s<GOAL>IsGLB s (sInf s)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : Set (WithTop α)<GOAL>IsGLB s (sInf s)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>hb : BddAbove s<GOAL>↑(sSup s) = ⨆ a ∈ s, ↑a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>h's : BddBelow s<GOAL>↑(sInf s) = ⨅ a ∈ s, ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>ConditionallyCompleteLattice β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>s : Set α<VAR>c : α<VAR>hcs : c ∈ s<VAR>h_bdd : BddAbove s<GOAL>f c ≤ sSup (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>ConditionallyCompleteLattice β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>B : α<VAR>hB : B ∈ upperBounds s<GOAL>sSup (f '' s) ≤ f B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>ConditionallyCompleteLattice β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>s : Set α<VAR>c : α<VAR>hcs : c ∈ s<VAR>h_bdd : BddBelow s<GOAL>sInf (f '' s) ≤ f c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>ConditionallyCompleteLattice β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>B : α<VAR>hB : B ∈ lowerBounds s<GOAL>f B ≤ sInf (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hbdd : BddAbove s<GOAL>l (sSup s) = ⨆ x, l ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hbdd : BddAbove s<GOAL>l (sSup s) = sSup (l '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>Nonempty ι<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>f : ι → α<VAR>hf : BddAbove (Set.range f)<GOAL>l (⨆ i, f i) = ⨆ i, l (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set γ<VAR>f : γ → α<VAR>hf : BddAbove (f '' s)<VAR>hne : s.Nonempty<GOAL>l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set β<VAR>hne : s.Nonempty<VAR>hbdd : BddBelow s<GOAL>u (sInf s) = ⨅ x, u ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set β<VAR>hne : s.Nonempty<VAR>hbdd : BddBelow s<GOAL>u (sInf s) = sInf (u '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>Nonempty ι<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>f : ι → β<VAR>hf : BddBelow (Set.range f)<GOAL>u (⨅ i, f i) = ⨅ i, u (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set γ<VAR>f : γ → β<VAR>hf : BddBelow (f '' s)<VAR>hne : s.Nonempty<GOAL>u (⨅ i, f ↑i) = ⨅ i, u (f ↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>e : α ≃o β<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hbdd : BddAbove s<GOAL>e (sSup s) = ⨆ x, e ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>e : α ≃o β<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hbdd : BddAbove s<GOAL>e (sSup s) = sSup (⇑e '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>Nonempty ι<VAR>e : α ≃o β<VAR>f : ι → α<VAR>hf : BddAbove (Set.range f)<GOAL>e (⨆ i, f i) = ⨆ i, e (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>e : α ≃o β<VAR>s : Set γ<VAR>f : γ → α<VAR>hf : BddAbove (f '' s)<VAR>hne : s.Nonempty<GOAL>e (⨆ i, f ↑i) = ⨆ i, e (f ↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>e : α ≃o β<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hbdd : BddBelow s<GOAL>e (sInf s) = ⨅ x, e ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>e : α ≃o β<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hbdd : BddBelow s<GOAL>e (sInf s) = sInf (⇑e '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>Nonempty ι<VAR>e : α ≃o β<VAR>f : ι → α<VAR>hf : BddBelow (Set.range f)<GOAL>e (⨅ i, f i) = ⨅ i, e (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>e : α ≃o β<VAR>s : Set γ<VAR>f : γ → α<VAR>hf : BddBelow (f '' s)<VAR>hne : s.Nonempty<GOAL>e (⨅ i, f ↑i) = ⨅ i, e (f ↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>ConditionallyCompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>l : α → β → γ<VAR>u₁ : β → γ → α<VAR>u₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddAbove s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddAbove t<GOAL>sSup (Set.image2 l s t) = l (sSup s) (sSup t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>ConditionallyCompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>l : α → β → γ<VAR>u₁ : β → γ → α<VAR>u₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)<GOAL>s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sSup (Set.image2 l s t) = l (sSup s) (sInf t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>ConditionallyCompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>l : α → β → γ<VAR>u₁ : β → γ → α<VAR>u₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)<GOAL>s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sSup (Set.image2 l s t) = l (sInf s) (sSup t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>ConditionallyCompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>l : α → β → γ<VAR>u₁ : β → γ → α<VAR>u₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)<GOAL>s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sSup (Set.image2 l s t) = l (sInf s) (sInf t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>ConditionallyCompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>u : α → β → γ<VAR>l₁ : β → γ → α<VAR>l₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)<GOAL>s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sInf (Set.image2 u s t) = u (sInf s) (sInf t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>ConditionallyCompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>u : α → β → γ<VAR>l₁ : β → γ → α<VAR>l₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)<VAR>h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual)<GOAL>s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sInf (Set.image2 u s t) = u (sInf s) (sSup t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>ConditionallyCompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>u : α → β → γ<VAR>l₁ : β → γ → α<VAR>l₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)<VAR>h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)<GOAL>s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sInf (Set.image2 u s t) = u (sSup s) (sInf t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>ConditionallyCompleteLattice β<VAR>ConditionallyCompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>u : α → β → γ<VAR>l₁ : β → γ → α<VAR>l₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)<VAR>h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual)<GOAL>s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sInf (Set.image2 u s t) = u (sSup s) (sSup t)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<GOAL>⨆ x, ↑(f x) = ⊤ ↔ ¬BddAbove (Set.range f)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<GOAL>⨆ x, ↑(f x) < ⊤ ↔ BddAbove (Set.range f)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<GOAL>⨅ x, ↑(f x) = ⊤ ↔ IsEmpty ι
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<GOAL>⨅ i, ↑(f i) < ⊤ ↔ Nonempty ι
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>x y : α × β<GOAL>Prod.GameAdd rα rβ x y ↔ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>Prod.GameAdd rα rβ (a₁, b₁) (a₂, b₂) ↔ rα a₁ a₂ ∧ b₁ = b₂ ∨ rβ b₁ b₂ ∧ a₁ = a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>a b : α × β<GOAL>Prod.GameAdd rβ rα a.swap b.swap ↔ Prod.GameAdd rα rβ a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>Prod.GameAdd rα rβ (a₁, b₁) (a₂, b₂) ↔ Prod.GameAdd rβ rα (b₁, a₁) (b₂, a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<GOAL>Prod.GameAdd rα rβ ≤ Prod.Lex rα rβ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<GOAL>Prod.RProd rα rβ ≤ Relation.TransGen (Prod.GameAdd rα rβ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>a : α<VAR>b : β<VAR>ha : Acc rα a<VAR>hb : Acc rβ b<GOAL>Acc (Prod.GameAdd rα rβ) (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>hα : WellFounded rα<VAR>hβ : WellFounded rβ<GOAL>WellFounded (Prod.GameAdd rα rβ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>C : α → β → Sort u_3<VAR>hα : WellFounded rα<VAR>hβ : WellFounded rβ<VAR>IH : (a₁ : α) → (b₁ : β) → ((a₂ : α) → (b₂ : β) → Prod.GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁<VAR>a : α<VAR>b : β<GOAL>Prod.GameAdd.fix hα hβ IH a b = IH a b fun a' b' x => Prod.GameAdd.fix hα hβ IH a' b'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>C : α → β → Prop<GOAL>WellFounded rα → WellFounded rβ → (∀ (a₁ : α) (b₁ : β), (∀ (a₂ : α) (b₂ : β), Prod.GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁) → ∀ (a : α) (b : β), C a b
<VAR>α : Type u_1<VAR>rα : α → α → Prop<VAR>x y : α × α<GOAL>Sym2.GameAdd rα (Sym2.mk x) (Sym2.mk y) ↔ Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα x.swap y
<VAR>α : Type u_1<VAR>rα : α → α → Prop<VAR>a₁ a₂ b₁ b₂ : α<GOAL>Sym2.GameAdd rα s(a₁, b₁) s(a₂, b₂) ↔ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)
<VAR>α : Type u_1<VAR>rα : α → α → Prop<VAR>a₁ a₂ b₁ b₂ : α<VAR>h : Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)<GOAL>Sym2.GameAdd rα s(a₁, b₁) s(a₂, b₂)
<VAR>α : Type u_1<VAR>rα : α → α → Prop<VAR>a₁ a₂ b : α<VAR>h : rα a₁ a₂<GOAL>Sym2.GameAdd rα s(a₁, b) s(a₂, b)
<VAR>α : Type u_1<VAR>rα : α → α → Prop<VAR>a b₁ b₂ : α<VAR>h : rα b₁ b₂<GOAL>Sym2.GameAdd rα s(a, b₁) s(a, b₂)
<VAR>α : Type u_1<VAR>rα : α → α → Prop<VAR>a₁ a₂ b : α<VAR>h : rα a₁ a₂<GOAL>Sym2.GameAdd rα s(a₁, b) s(b, a₂)
<VAR>α : Type u_1<VAR>rα : α → α → Prop<VAR>a₁ a₂ b : α<VAR>h : rα a₁ a₂<GOAL>Sym2.GameAdd rα s(b, a₁) s(a₂, b)
<VAR>α : Type u_1<VAR>rα : α → α → Prop<VAR>a b : α<VAR>ha : Acc rα a<VAR>hb : Acc rα b<GOAL>Acc (Sym2.GameAdd rα) s(a, b)
<VAR>α : Type u_1<VAR>rα : α → α → Prop<VAR>h : WellFounded rα<GOAL>WellFounded (Sym2.GameAdd rα)
<VAR>α : Type u_1<VAR>rα : α → α → Prop<VAR>C : α → α → Sort u_3<VAR>hr : WellFounded rα<VAR>IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁<VAR>a b : α<GOAL>Sym2.GameAdd.fix hr IH a b = IH a b fun a' b' x => Sym2.GameAdd.fix hr IH a' b'
<VAR>α : Type u_1<VAR>rα C : α → α → Prop<GOAL>WellFounded rα → (∀ (a₁ b₁ : α), (∀ (a₂ b₂ : α), Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) → ∀ (a b : α), C a b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>self : CompleteSublattice α<VAR>s : Set α<GOAL>s ⊆ self.carrier → sSup s ∈ self.carrier
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>self : CompleteSublattice α<VAR>s : Set α<GOAL>s ⊆ self.carrier → sInf s ∈ self.carrier
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>carrier : Set α<VAR>sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier<VAR>sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier<GOAL>(CompleteSublattice.mk' carrier sSupClosed' sInfClosed').carrier = carrier
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<VAR>s : Set α<VAR>h : s ⊆ ↑L<GOAL>sSup s ∈ L
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<VAR>s : Set α<VAR>h : s ⊆ ↑L<GOAL>sInf s ∈ L
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<GOAL>↑⊥ = ⊥
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<GOAL>↑⊤ = ⊤
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<VAR>S : Set ↥L<GOAL>↑(sSup S) = sSup {x | ∃ s ∈ S, ↑s = x}
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<VAR>S : Set ↥L<GOAL>↑(sSup S) = ⨆ N ∈ S, ↑N
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<VAR>S : Set ↥L<GOAL>↑(sInf S) = sInf {x | ∃ s ∈ S, ↑s = x}
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<VAR>S : Set ↥L<GOAL>↑(sInf S) = ⨅ N ∈ S, ↑N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L : CompleteSublattice α<GOAL>(CompleteSublattice.map f L).carrier = ⇑f '' ↑L
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L : CompleteSublattice α<VAR>b : β<GOAL>b ∈ CompleteSublattice.map f L ↔ ∃ a ∈ L, f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L : CompleteSublattice β<GOAL>(CompleteSublattice.comap f L).carrier = ⇑f ⁻¹' ↑L
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L : CompleteSublattice β<VAR>a : α<GOAL>a ∈ CompleteSublattice.comap f L ↔ f a ∈ L
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<VAR>a b : ↥L<GOAL>Disjoint a b ↔ Disjoint ↑a ↑b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<VAR>a b : ↥L<GOAL>Codisjoint a b ↔ Codisjoint ↑a ↑b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<VAR>a b : ↥L<GOAL>IsCompl a b ↔ IsCompl ↑a ↑b