ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Monotone f<GOAL>⨆ a ∈ s, f a ≤ f (sSup s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Antitone f<GOAL>⨆ a ∈ s, f a ≤ f (sInf s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α ≃o β<VAR>x : ι → α<GOAL>f (⨆ i, x i) = ⨆ i, f (x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α ≃o β<VAR>x : ι → α<GOAL>f (⨅ i, x i) = ⨅ i, f (x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α ≃o β<VAR>s : Set α<GOAL>f (sSup s) = ⨆ a ∈ s, f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α ≃o β<VAR>s : Set α<GOAL>f (sInf s) = ⨅ a ∈ s, f a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>ι' : Sort u_9<VAR>f : ι' → α<VAR>g : ι → ι'<GOAL>⨆ x, f (g x) ≤ ⨆ y, f y
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>ι' : Sort u_9<VAR>f : ι' → α<VAR>g : ι → ι'<GOAL>⨅ y, f y ≤ ⨅ x, f (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>Preorder β<VAR>f : β → α<VAR>hf : Monotone f<VAR>s : ι → β<VAR>hs : ∀ (x : β), ∃ i, x ≤ s i<GOAL>⨆ x, f (s x) = ⨆ y, f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>Preorder β<VAR>f : β → α<VAR>hf : Monotone f<VAR>s : ι → β<VAR>hs : ∀ (x : β), ∃ i, s i ≤ x<GOAL>⨅ x, f (s x) = ⨅ y, f y
<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>f (iSup s) ≤ ⨅ i, f (s i)
<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>f (iInf s) ≤ ⨅ i, f (s i)
<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>f (⨆ i, ⨆ j, s i j) ≤ ⨅ i, ⨅ j, f (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 : Monotone f<VAR>s : (i : ι) → κ i → α<GOAL>f (⨅ i, ⨅ j, s i j) ≤ ⨅ i, ⨅ j, f (s i j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Antitone f<GOAL>f (sSup s) ≤ ⨅ a ∈ s, f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Monotone f<GOAL>f (sInf s) ≤ ⨅ a ∈ s, f a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>a : α<GOAL>⨆ x, a ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>a : α<GOAL>a ≤ ⨅ x, a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>a : α<VAR>Nonempty ι<GOAL>⨆ x, a = a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>a : α<VAR>Nonempty ι<GOAL>⨅ x, a = a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>Unique ι<VAR>f : ι → α<GOAL>⨆ i, f i = f default
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>Unique ι<VAR>f : ι → α<GOAL>⨅ i, f i = f default
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<GOAL>⨆ x, ⊥ = ⊥
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<GOAL>⨅ x, ⊤ = ⊤
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>s : ι → α<GOAL>iSup s = ⊥ ↔ ∀ (i : ι), s i = ⊥
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>s : ι → α<GOAL>iInf s = ⊤ ↔ ∀ (i : ι), s i = ⊤
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>f : (i : ι) → κ i → α<GOAL>⨆ i, ⨆ j, f i j = ⊥ ↔ ∀ (i : ι) (j : κ i), f i j = ⊥
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_7<VAR>CompleteLattice α<VAR>f : (i : ι) → κ i → α<GOAL>⨅ i, ⨅ j, f i j = ⊤ ↔ ∀ (i : ι) (j : κ i), f i j = ⊤
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p : Prop<VAR>f : p → α<VAR>hp : p<GOAL>⨆ (h : p), f h = f hp
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p : Prop<VAR>f : p → α<VAR>hp : p<GOAL>⨅ (h : p), f h = f hp
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p : Prop<VAR>f : p → α<VAR>hp : ¬p<GOAL>⨆ (h : p), f h = ⊥
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p : Prop<VAR>f : p → α<VAR>hp : ¬p<GOAL>⨅ (h : p), f h = ⊤
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>b : α<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_5<VAR>CompleteLattice α<VAR>f : ι → α<VAR>b : α<GOAL>(∀ (i : ι), b ≤ f i) → (∀ (w : α), b < w → ∃ i, f i < w) → ⨅ i, f i = b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p : Prop<VAR>Decidable p<VAR>a : p → α<GOAL>⨆ (h : p), a h = if h : p then a h else ⊥
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p : Prop<VAR>Decidable p<VAR>a : α<GOAL>⨆ (_ : p), a = if p then a else ⊥
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p : Prop<VAR>Decidable p<VAR>a : p → α<GOAL>⨅ (h : p), a h = if h : p then a h else ⊤
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p : Prop<VAR>Decidable p<VAR>a : α<GOAL>⨅ (_ : p), a = if p then a else ⊤
<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>ι' : Sort u_6<VAR>CompleteLattice α<VAR>f : ι → ι' → α<GOAL>⨅ i, ⨅ j, f i j = ⨅ j, ⨅ i, f i j
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι₁ : Sort u_9<VAR>ι₂ : Sort u_10<VAR>κ₁ : ι₁ → Sort u_11<VAR>κ₂ : ι₂ → Sort u_12<VAR>f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α<GOAL>⨆ i₁, ⨆ j₁, ⨆ i₂, ⨆ j₂, f i₁ j₁ i₂ j₂ = ⨆ i₂, ⨆ j₂, ⨆ i₁, ⨆ j₁, f i₁ j₁ i₂ j₂
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι₁ : Sort u_9<VAR>ι₂ : Sort u_10<VAR>κ₁ : ι₁ → Sort u_11<VAR>κ₂ : ι₂ → Sort u_12<VAR>f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α<GOAL>⨅ i₁, ⨅ j₁, ⨅ i₂, ⨅ j₂, f i₁ j₁ i₂ j₂ = ⨅ i₂, ⨅ j₂, ⨅ i₁, ⨅ j₁, f i₁ j₁ i₂ j₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>b : β<VAR>f : (x : β) → x = b → α<GOAL>⨆ x, ⨆ (h : x = b), f x h = f b ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>b : β<VAR>f : (x : β) → x = b → α<GOAL>⨅ x, ⨅ (h : x = b), f x h = f b ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>b : β<VAR>f : (x : β) → b = x → α<GOAL>⨆ x, ⨆ (h : b = x), f x h = f b ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>b : β<VAR>f : (x : β) → b = x → α<GOAL>⨅ x, ⨅ (h : b = x), f x h = f b ⋯
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>f : Subtype p → α<GOAL>iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>f : Subtype p → α<GOAL>iInf f = ⨅ i, ⨅ (h : p i), f ⟨i, h⟩
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<GOAL>⨆ i, ⨆ (h : p i), f i h = ⨆ x, f ↑x ⋯
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<GOAL>⨅ i, ⨅ (h : p i), f i h = ⨅ x, f ↑x ⋯
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι : Type u_9<VAR>s : Set ι<VAR>f : ι → α<GOAL>⨆ i, f ↑i = ⨆ t ∈ s, f t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι : Type u_9<VAR>s : Set ι<VAR>f : ι → α<GOAL>⨅ i, f ↑i = ⨅ t ∈ s, f t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι : Type u_9<VAR>a : α<VAR>s : Set ι<VAR>hs : s.Nonempty<GOAL>⨆ i ∈ s, a = a
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι : Type u_9<VAR>a : α<VAR>s : Set ι<VAR>hs : s.Nonempty<GOAL>⨅ i ∈ s, a = a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f g : ι → α<GOAL>⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f g : ι → α<GOAL>⨅ x, f x ⊓ g x = (⨅ x, f x) ⊓ ⨅ x, g x
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι : Type u_9<VAR>ι' : Type u_10<VAR>g : ι' → α<VAR>e : ι ≃ ι'<VAR>s : Set ι'<GOAL>⨆ i ∈ ⇑e.symm '' s, g (e i) = ⨆ i ∈ s, g i
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι : Type u_9<VAR>ι' : Type u_10<VAR>g : ι' → α<VAR>e : ι ≃ ι'<VAR>s : Set ι'<GOAL>⨅ i ∈ ⇑e.symm '' s, g (e i) = ⨅ i ∈ s, g i
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι : Type u_9<VAR>s : Set ι<VAR>f : ι → α<VAR>i : ι<VAR>hi : i ∈ s<GOAL>⨅ i ∈ s, f i ≤ f i
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι : Type u_9<VAR>s : Set ι<VAR>f : ι → α<VAR>i : ι<VAR>hi : i ∈ s<GOAL>f i ≤ ⨆ i ∈ s, f i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>Nonempty ι<VAR>f : ι → α<VAR>a : α<GOAL>(⨆ x, f x) ⊔ a = ⨆ x, f x ⊔ a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>Nonempty ι<VAR>f : ι → α<VAR>a : α<GOAL>(⨅ x, f x) ⊓ a = ⨅ x, f x ⊓ a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>Nonempty ι<VAR>f : ι → α<VAR>a : α<GOAL>a ⊔ ⨆ x, f x = ⨆ x, a ⊔ f x
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>Nonempty ι<VAR>f : ι → α<VAR>a : α<GOAL>a ⊓ ⨅ x, f x = ⨅ x, a ⊓ f x
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<VAR>a : α<VAR>h : ∃ i, p i<GOAL>(⨆ i, ⨆ (h : p i), f i h) ⊔ a = ⨆ i, ⨆ (h : p i), f i h ⊔ a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<VAR>a : α<VAR>h : ∃ i, p i<GOAL>a ⊔ ⨆ i, ⨆ (h : p i), f i h = ⨆ i, ⨆ (h : p i), a ⊔ f i h
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<VAR>a : α<VAR>h : ∃ i, p i<GOAL>(⨅ i, ⨅ (h : p i), f i h) ⊓ a = ⨅ i, ⨅ (h : p i), f i h ⊓ a
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<VAR>a : α<VAR>h : ∃ i, p i<GOAL>a ⊓ ⨅ i, ⨅ (h : p i), f i h = ⨅ i, ⨅ (h : p i), a ⊓ f i h
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : False → α<GOAL>iSup s = ⊥
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : False → α<GOAL>iInf s = ⊤
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : True → α<GOAL>iSup s = s trivial
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : True → α<GOAL>iInf s = s trivial
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>f : Exists p → α<GOAL>⨆ (x : Exists p), f x = ⨆ i, ⨆ (h : p i), f ⋯
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>f : Exists p → α<GOAL>⨅ (x : Exists p), f x = ⨅ i, ⨅ (h : p i), f ⋯
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p q : Prop<VAR>s : p ∧ q → α<GOAL>iSup s = ⨆ (h₁ : p), ⨆ (h₂ : q), s ⋯
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p q : Prop<VAR>s : p ∧ q → α<GOAL>iInf s = ⨅ (h₁ : p), ⨅ (h₂ : q), s ⋯
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p q : Prop<VAR>s : p → q → α<GOAL>⨆ (h₁ : p), ⨆ (h₂ : q), s h₁ h₂ = ⨆ (h : p ∧ q), s ⋯ ⋯
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p q : Prop<VAR>s : p → q → α<GOAL>⨅ (h₁ : p), ⨅ (h₂ : q), s h₁ h₂ = ⨅ (h : p ∧ q), s ⋯ ⋯
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p q : Prop<VAR>s : p ∨ q → α<GOAL>⨆ (x : p ∨ q), s x = (⨆ (i : p), s ⋯) ⊔ ⨆ (j : q), s ⋯
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p q : Prop<VAR>s : p ∨ q → α<GOAL>⨅ (x : p ∨ q), s x = (⨅ (i : p), s ⋯) ⊓ ⨅ (j : q), s ⋯
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f : (i : ι) → p i → α<VAR>g : (i : ι) → ¬p i → α<GOAL>(⨆ i, if h : p i then f i h else g i h) = (⨆ i, ⨆ (h : p i), f i h) ⊔ ⨆ i, ⨆ (h : ¬p i), g i h
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f : (i : ι) → p i → α<VAR>g : (i : ι) → ¬p i → α<GOAL>(⨅ i, if h : p i then f i h else g i h) = (⨅ i, ⨅ (h : p i), f i h) ⊓ ⨅ i, ⨅ (h : ¬p i), g i h
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f g : ι → α<GOAL>(⨆ i, if p i then f i else g i) = (⨆ i, ⨆ (_ : p i), f i) ⊔ ⨆ i, ⨆ (_ : ¬p i), g i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f g : ι → α<GOAL>(⨅ i, if p i then f i else g i) = (⨅ i, ⨅ (_ : p i), f i) ⊓ ⨅ i, ⨅ (_ : ¬p i), g i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>g : β → α<VAR>f : ι → β<GOAL>⨆ b ∈ Set.range f, g b = ⨆ i, g (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>g : β → α<VAR>f : ι → β<GOAL>⨅ b ∈ Set.range f, g b = ⨅ i, g (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>s : Set β<VAR>f : β → α<GOAL>sSup (f '' s) = ⨆ a ∈ s, f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>s : Set β<VAR>f : β → α<GOAL>sInf (f '' s) = ⨅ a ∈ s, f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α ≃o β<VAR>s : Set α<GOAL>f (sSup s) = sSup (⇑f.symm ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α ≃o β<VAR>s : Set α<GOAL>f (sInf s) = sInf (⇑f.symm ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<GOAL>⨆ x ∈ ∅, f x = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<GOAL>⨅ x ∈ ∅, f x = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<GOAL>⨆ x ∈ Set.univ, f x = ⨆ x, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<GOAL>⨅ x ∈ Set.univ, f x = ⨅ x, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>s t : Set β<GOAL>⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>s t : Set β<GOAL>⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ ⨅ x ∈ t, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>p : β → Prop<GOAL>⨆ i, f i = (⨆ i, ⨆ (_ : p i), f i) ⊔ ⨆ i, ⨆ (_ : ¬p i), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>p : β → Prop<GOAL>⨅ i, f i = (⨅ i, ⨅ (_ : p i), f i) ⊓ ⨅ i, ⨅ (_ : ¬p i), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>i₀ : β<GOAL>⨆ i, f i = f i₀ ⊔ ⨆ i, ⨆ (_ : i ≠ i₀), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>i₀ : β<GOAL>⨅ i, f i = f i₀ ⊓ ⨅ i, ⨅ (_ : i ≠ i₀), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>s t : Set β<GOAL>s ⊆ t → ⨆ x ∈ s, f x ≤ ⨆ x ∈ t, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>s t : Set β<GOAL>s ⊆ t → ⨅ x ∈ t, f x ≤ ⨅ x ∈ s, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>s : Set β<VAR>b : β<GOAL>⨆ x ∈ insert b s, f x = f b ⊔ ⨆ x ∈ s, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>s : Set β<VAR>b : β<GOAL>⨅ x ∈ insert b s, f x = f b ⊓ ⨅ x ∈ s, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>b : β<GOAL>⨆ x ∈ {b}, f x = f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>b : β<GOAL>⨅ x ∈ {b}, f x = f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>a b : β<GOAL>⨆ x ∈ {a, b}, f x = f a ⊔ f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<VAR>a b : β<GOAL>⨅ x ∈ {a, b}, f x = f a ⊓ f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>γ : Type u_9<VAR>f : β → γ<VAR>g : γ → α<VAR>t : Set β<GOAL>⨆ c ∈ f '' t, g c = ⨆ b ∈ t, g (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>γ : Type u_9<VAR>f : β → γ<VAR>g : γ → α<VAR>t : Set β<GOAL>⨅ c ∈ f '' t, g c = ⨅ b ∈ t, g (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>e : ι → β<VAR>he : Function.Injective e<VAR>f : ι → α<GOAL>⨆ j, Function.extend e f ⊥ j = ⨆ i, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>e : ι → β<VAR>he : Function.Injective e<VAR>f : ι → α<GOAL>⨅ j, Function.extend e f ⊤ j = iInf f
<VAR>α : Type u_9<VAR>ι : Sort u_10<VAR>SupSet α<VAR>IsEmpty ι<VAR>f : ι → α<GOAL>iSup f = sSup ∅
<VAR>α : Type u_9<VAR>ι : Sort u_10<VAR>InfSet α<VAR>IsEmpty ι<VAR>f : ι → α<GOAL>iInf f = sInf ∅
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>IsEmpty ι<VAR>f : ι → α<GOAL>iSup f = ⊥
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>IsEmpty ι<VAR>f : ι → α<GOAL>iInf f = ⊤
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : Bool → α<GOAL>⨆ b, f b = f true ⊔ f false
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : Bool → α<GOAL>⨅ b, f b = f true ⊓ f false
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>x y : α<GOAL>x ⊔ y = ⨆ b, bif b then x else y
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>x y : α<GOAL>x ⊓ y = ⨅ b, bif b then x else y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>s : Set β<VAR>f : β → α<GOAL>IsGLB (f '' s) (⨅ x ∈ s, f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>s : Set β<VAR>f : β → α<GOAL>IsLUB (f '' s) (⨆ x ∈ s, f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>p : β → Type u_9<VAR>f : Sigma p → α<GOAL>⨆ x, f x = ⨆ i, ⨆ j, f ⟨i, j⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>p : β → Type u_9<VAR>f : Sigma p → α<GOAL>⨅ x, f x = ⨅ i, ⨅ j, f ⟨i, j⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>κ : β → Type u_9<VAR>f : (i : β) → κ i → α<GOAL>⨆ i, ⨆ j, f i j = ⨆ x, f x.fst x.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>κ : β → Type u_9<VAR>f : (i : β) → κ i → α<GOAL>⨅ i, ⨅ j, f i j = ⨅ x, f x.fst x.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>f : β × γ → α<GOAL>⨆ x, f x = ⨆ i, ⨆ j, f (i, j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>f : β × γ → α<GOAL>⨅ x, f x = ⨅ i, ⨅ j, f (i, j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>f : β → γ → α<GOAL>⨆ i, ⨆ j, f i j = ⨆ x, f x.1 x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>f : β → γ → α<GOAL>⨅ i, ⨅ j, f i j = ⨅ x, f x.1 x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>f : β × γ → α<VAR>s : Set β<VAR>t : Set γ<GOAL>⨆ x ∈ s ×ˢ t, f x = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>f : β × γ → α<VAR>s : Set β<VAR>t : Set γ<GOAL>⨅ x ∈ s ×ˢ t, f x = ⨅ a ∈ s, ⨅ b ∈ t, f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>f : β ⊕ γ → α<GOAL>⨆ x, f x = (⨆ i, f (Sum.inl i)) ⊔ ⨆ j, f (Sum.inr j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>f : β ⊕ γ → α<GOAL>⨅ x, f x = (⨅ i, f (Sum.inl i)) ⊓ ⨅ j, f (Sum.inr j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Option β → α<GOAL>⨆ o, f o = f none ⊔ ⨆ b, f (some b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Option β → α<GOAL>⨅ o, f o = f none ⊓ ⨅ b, f (some b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>a : α<VAR>f : β → α<GOAL>⨆ o, o.elim a f = a ⊔ ⨆ b, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>a : α<VAR>f : β → α<GOAL>⨅ o, o.elim a f = a ⊓ ⨅ b, f b
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<GOAL>⨆ i, f ↑i = ⨆ i, f i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>f : ι → α<GOAL>⨅ i, f ↑i = ⨅ i, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>f : β → γ → α<VAR>s : Set β<VAR>t : Set γ<GOAL>sSup (Set.image2 f s t) = ⨆ a ∈ s, ⨆ b ∈ t, f a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>f : β → γ → α<VAR>s : Set β<VAR>t : Set γ<GOAL>sInf (Set.image2 f s t) = ⨅ a ∈ s, ⨅ b ∈ t, f a b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨆ i, ⨆ (_ : i ≥ n), u i = ⨆ i, u (i + n)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨅ i, ⨅ (_ : i ≥ n), u i = ⨅ i, u (i + n)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : ℕ → α<VAR>hf : Monotone f<VAR>k : ℕ<GOAL>⨆ n, f (n + k) = ⨆ n, f n
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : ℕ → α<VAR>hf : Antitone f<VAR>k : ℕ<GOAL>⨅ n, f (n + k) = ⨅ n, f n
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : ℕ → α<VAR>k : ℕ<GOAL>⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : ℕ → α<VAR>k : ℕ<GOAL>⨅ n, ⨆ i, ⨆ (_ : i ≥ n), f (i + k) = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), f i
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<GOAL>u 0 ⊔ ⨆ i, u (i + 1) = ⨆ i, u i
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<GOAL>u 0 ⊓ ⨅ i, u (i + 1) = ⨅ i, u i
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : ℕ → α<GOAL>⨅ i, ⨅ (_ : i > 0), f i = ⨅ i, f (i + 1)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : ℕ → α<GOAL>⨆ i, ⨆ (_ : i > 0), f i = ⨆ i, f (i + 1)
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLinearOrder α<VAR>f : ι → α<GOAL>iSup f = ⊤ ↔ ∀ b < ⊤, ∃ i, b < f i
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLinearOrder α<VAR>f : ι → α<GOAL>iInf f = ⊥ ↔ ∀ b > ⊥, ∃ i, f i < b
<VAR>s : Set Prop<GOAL>sSup s = ∃ p ∈ s, p
<VAR>s : Set Prop<GOAL>sInf s = ∀ p ∈ s, p
<VAR>ι : Sort u_5<VAR>p : ι → Prop<GOAL>⨆ i, p i = ∃ i, p i
<VAR>ι : Sort u_5<VAR>p : ι → Prop<GOAL>⨅ i, p i = ∀ (i : ι), p i
<VAR>α : Type u_9<VAR>β : α → Type u_10<VAR>(i : α) → SupSet (β i)<VAR>s : Set ((a : α) → β a)<VAR>a : α<GOAL>sSup s a = ⨆ f, ↑f a
<VAR>α : Type u_9<VAR>β : α → Type u_10<VAR>(i : α) → InfSet (β i)<VAR>s : Set ((a : α) → β a)<VAR>a : α<GOAL>sInf s a = ⨅ f, ↑f a
<VAR>α : Type u_9<VAR>β : α → Type u_10<VAR>ι : Sort u_11<VAR>(i : α) → SupSet (β i)<VAR>f : ι → (a : α) → β a<VAR>a : α<GOAL>(⨆ i, f i) a = ⨆ i, f i a
<VAR>α : Type u_9<VAR>β : α → Type u_10<VAR>ι : Sort u_11<VAR>(i : α) → InfSet (β i)<VAR>f : ι → (a : α) → β a<VAR>a : α<GOAL>(⨅ i, f i) a = ⨅ i, f i a
<VAR>α : Type u_9<VAR>s : Set (α → Prop)<VAR>a : α<GOAL>sSup s a ↔ ∃ r ∈ s, r a
<VAR>α : Type u_9<VAR>s : Set (α → Prop)<VAR>a : α<GOAL>sInf s a ↔ ∀ r ∈ s, r a
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>s : Set (α → β → Prop)<VAR>a : α<VAR>b : β<GOAL>sSup s a b ↔ ∃ r ∈ s, r a b
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>s : Set (α → β → Prop)<VAR>a : α<VAR>b : β<GOAL>sInf s a b ↔ ∀ r ∈ s, r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>CompleteLattice β<VAR>s : Set (α → β)<VAR>hs : ∀ f ∈ s, Monotone f<GOAL>Monotone (sSup s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>CompleteLattice β<VAR>s : Set (α → β)<VAR>hs : ∀ f ∈ s, Monotone f<GOAL>Monotone (sInf s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>CompleteLattice β<VAR>s : Set (α → β)<VAR>hs : ∀ f ∈ s, Antitone f<GOAL>Antitone (sSup s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>CompleteLattice β<VAR>s : Set (α → β)<VAR>hs : ∀ f ∈ s, Antitone f<GOAL>Antitone (sInf s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_9<VAR>Preorder α<VAR>CompleteLattice β<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Monotone (f i)<GOAL>Monotone (⨆ i, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_9<VAR>Preorder α<VAR>CompleteLattice β<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Monotone (f i)<GOAL>Monotone (⨅ i, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_9<VAR>Preorder α<VAR>CompleteLattice β<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Antitone (f i)<GOAL>Antitone (⨆ i, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_9<VAR>Preorder α<VAR>CompleteLattice β<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Antitone (f i)<GOAL>Antitone (⨅ i, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>InfSet α<VAR>InfSet β<VAR>s : Set (α × β)<GOAL>(sInf s).1 = sInf (Prod.fst '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>InfSet α<VAR>InfSet β<VAR>s : Set (α × β)<GOAL>(sInf s).2 = sInf (Prod.snd '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>InfSet α<VAR>InfSet β<VAR>s : Set (α × β)<GOAL>(sInf s).swap = sInf (Prod.swap '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SupSet α<VAR>SupSet β<VAR>s : Set (α × β)<GOAL>(sSup s).1 = sSup (Prod.fst '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SupSet α<VAR>SupSet β<VAR>s : Set (α × β)<GOAL>(sSup s).2 = sSup (Prod.snd '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SupSet α<VAR>SupSet β<VAR>s : Set (α × β)<GOAL>(sSup s).swap = sSup (Prod.swap '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>InfSet α<VAR>InfSet β<VAR>f : ι → α × β<GOAL>(iInf f).1 = ⨅ i, (f i).1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>InfSet α<VAR>InfSet β<VAR>f : ι → α × β<GOAL>(iInf f).2 = ⨅ i, (f i).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>InfSet α<VAR>InfSet β<VAR>f : ι → α × β<GOAL>(iInf f).swap = ⨅ i, (f i).swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_5<VAR>InfSet α<VAR>InfSet β<VAR>f : ι → α<VAR>g : ι → β<GOAL>⨅ i, (f i, g i) = (⨅ i, f i, ⨅ i, g i)