ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>h : WellFounded fun x x_1 => x < x_1<GOAL>IsStronglyAtomic α
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>h : WellFounded fun x x_1 => x > x_1<GOAL>IsStronglyCoatomic α
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderBot α<VAR>h : WellFounded fun x x_1 => x < x_1<GOAL>IsAtomic α
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderTop α<VAR>h : WellFounded fun x x_1 => x > x_1<GOAL>IsCoatomic α
<VAR>α : Type u_4<VAR>BooleanAlgebra α<VAR>IsAtomic α<VAR>x y : α<GOAL>x ≤ y ↔ ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
<VAR>α : Type u_4<VAR>BooleanAlgebra α<VAR>IsAtomic α<VAR>x y : α<GOAL>x = y ↔ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>self : IsAtomistic α<VAR>b : α<GOAL>∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>self : IsCoatomistic α<VAR>b : α<GOAL>∃ s, b = sInf s ∧ ∀ a ∈ s, IsCoatom a
<VAR>α : Type u_2<VAR>CompleteLattice α<GOAL>IsCoatomistic αᵒᵈ ↔ IsAtomistic α
<VAR>α : Type u_2<VAR>CompleteLattice α<GOAL>IsAtomistic αᵒᵈ ↔ IsCoatomistic α
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsAtomistic α<VAR>b : α<GOAL>sSup {a | IsAtom a ∧ a ≤ b} = b
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsAtomistic α<GOAL>sSup {a | IsAtom a} = ⊤
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsAtomistic α<VAR>a b : α<GOAL>a ≤ b ↔ ∀ (c : α), IsAtom c → c ≤ a → c ≤ b
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsAtomistic α<VAR>a b : α<GOAL>a = b ↔ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
<VAR>α : Type u_4<VAR>LE α<VAR>BoundedOrder α<VAR>self : IsSimpleOrder α<VAR>a : α<GOAL>a = ⊥ ∨ a = ⊤
<VAR>α : Type u_2<VAR>LE α<VAR>BoundedOrder α<GOAL>IsSimpleOrder α ↔ IsSimpleOrder αᵒᵈ
<VAR>α : Type u_2<VAR>LE α<VAR>BoundedOrder α<VAR>IsSimpleOrder α<GOAL>⊥ ≠ ⊤
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>IsSimpleOrder α<GOAL>IsAtom ⊤
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>IsSimpleOrder α<GOAL>IsCoatom ⊥
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>IsSimpleOrder α<GOAL>⊥ ⋖ ⊤
<VAR>α : Type u_2<VAR>Preorder α<VAR>BoundedOrder α<VAR>IsSimpleOrder α<VAR>a b : α<VAR>h : a < b<GOAL>a = ⊥
<VAR>α : Type u_2<VAR>Preorder α<VAR>BoundedOrder α<VAR>IsSimpleOrder α<VAR>a b : α<VAR>h : a < b<GOAL>b = ⊤
<VAR>α : Type u_4<VAR>DecidableEq α<VAR>LE α<VAR>BoundedOrder α<VAR>IsSimpleOrder α<VAR>x : Bool<GOAL>IsSimpleOrder.equivBool.symm x = Bool.casesOn x ⊥ ⊤
<VAR>α : Type u_4<VAR>DecidableEq α<VAR>LE α<VAR>BoundedOrder α<VAR>IsSimpleOrder α<VAR>x : α<GOAL>IsSimpleOrder.equivBool x = decide (x = ⊤)
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>BoundedOrder α<GOAL>IsSimpleOrder α ↔ IsAtom ⊤
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>BoundedOrder α<GOAL>IsSimpleOrder α ↔ IsCoatom ⊥
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>IsSimpleOrder ↑(Set.Iic a) ↔ IsAtom a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>IsSimpleOrder ↑(Set.Ici a) ↔ IsCoatom a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderBot α<VAR>OrderBot β<VAR>f : β ↪o α<VAR>hbot : f ⊥ = ⊥<VAR>b : β<VAR>hb : IsAtom (f b)<GOAL>IsAtom b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderTop α<VAR>OrderTop β<VAR>f : β ↪o α<VAR>htop : f ⊤ = ⊤<VAR>b : β<VAR>hb : IsCoatom (f b)<GOAL>IsCoatom b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderBot α<VAR>OrderBot β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>hbot : u ⊥ = ⊥<VAR>b : β<VAR>hb : IsAtom (u b)<GOAL>IsAtom b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderBot α<VAR>IsAtomic α<VAR>OrderBot β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>hbot : u ⊥ = ⊥<VAR>h_atom : ∀ (a : α), IsAtom a → u (l a) = a<VAR>a : α<GOAL>IsAtom (l a) ↔ IsAtom a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderBot α<VAR>IsAtomic α<VAR>OrderBot β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>hbot : u ⊥ = ⊥<VAR>h_atom : ∀ (a : α), IsAtom a → u (l a) = a<VAR>b : β<GOAL>IsAtom (u b) ↔ IsAtom b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderTop α<VAR>OrderTop β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>b : β<VAR>hb : IsCoatom (u b)<GOAL>IsCoatom b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderTop α<VAR>IsCoatomic α<VAR>OrderTop β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a<VAR>b : β<GOAL>IsCoatom (u b) ↔ IsCoatom b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderTop α<VAR>OrderTop β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisCoinsertion l u<VAR>hbot : l ⊤ = ⊤<VAR>a : α<VAR>hb : IsCoatom (l a)<GOAL>IsCoatom a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderTop α<VAR>OrderTop β<VAR>IsCoatomic β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisCoinsertion l u<VAR>htop : l ⊤ = ⊤<VAR>h_coatom : ∀ (b : β), IsCoatom b → l (u b) = b<VAR>b : β<GOAL>IsCoatom (u b) ↔ IsCoatom b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderTop α<VAR>OrderTop β<VAR>IsCoatomic β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisCoinsertion l u<VAR>htop : l ⊤ = ⊤<VAR>h_coatom : ∀ (b : β), IsCoatom b → l (u b) = b<VAR>a : α<GOAL>IsCoatom (l a) ↔ IsCoatom a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderBot α<VAR>OrderBot β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisCoinsertion l u<VAR>a : α<VAR>hb : IsAtom (l a)<GOAL>IsAtom a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderBot α<VAR>OrderBot β<VAR>IsAtomic β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisCoinsertion l u<VAR>h_atom : ∀ (b : β), IsAtom b → l (u b) = b<VAR>a : α<GOAL>IsAtom (l a) ↔ IsAtom a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderBot α<VAR>OrderBot β<VAR>f : α ≃o β<VAR>a : α<GOAL>IsAtom (f a) ↔ IsAtom a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderTop α<VAR>OrderTop β<VAR>f : α ≃o β<VAR>a : α<GOAL>IsCoatom (f a) ↔ IsCoatom a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : α ≃o β<GOAL>IsSimpleOrder α ↔ IsSimpleOrder β
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>h : IsSimpleOrder β<VAR>f : α ≃o β<GOAL>IsSimpleOrder α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderBot α<VAR>OrderBot β<VAR>f : α ≃o β<GOAL>IsAtomic α ↔ IsAtomic β
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderTop α<VAR>OrderTop β<VAR>f : α ≃o β<GOAL>IsCoatomic α ↔ IsCoatomic β
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsUpperModularLattice α<VAR>IsAtomistic α<GOAL>IsStronglyAtomic α
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsLowerModularLattice α<VAR>IsCoatomistic α<GOAL>IsStronglyCoatomic α
<VAR>α : Type u_2<VAR>Lattice α<VAR>BoundedOrder α<VAR>IsModularLattice α<VAR>a b : α<VAR>hc : IsCompl a b<GOAL>IsAtom a ↔ IsCoatom b
<VAR>α : Type u_2<VAR>Lattice α<VAR>BoundedOrder α<VAR>IsModularLattice α<VAR>a b : α<VAR>hc : IsCompl a b<GOAL>IsCoatom a ↔ IsAtom b
<VAR>α : Type u_2<VAR>Lattice α<VAR>BoundedOrder α<VAR>IsModularLattice α<VAR>ComplementedLattice α<VAR>IsAtomic α<GOAL>IsCoatomic α
<VAR>α : Type u_2<VAR>Lattice α<VAR>BoundedOrder α<VAR>IsModularLattice α<VAR>ComplementedLattice α<VAR>IsCoatomic α<GOAL>IsAtomic α
<VAR>α : Type u_2<VAR>Lattice α<VAR>BoundedOrder α<VAR>IsModularLattice α<VAR>ComplementedLattice α<GOAL>IsAtomic α ↔ IsCoatomic α
<VAR>α : Type u_2<VAR>Lattice α<VAR>BoundedOrder α<VAR>IsModularLattice α<VAR>ComplementedLattice α<VAR>IsAtomic α<GOAL>IsStronglyAtomic α
<VAR>α : Type u_2<VAR>Lattice α<VAR>BoundedOrder α<VAR>IsModularLattice α<VAR>ComplementedLattice α<VAR>IsCoatomic α<GOAL>IsStronglyCoatomic α
<VAR>α : Type u_2<VAR>Lattice α<VAR>BoundedOrder α<VAR>IsModularLattice α<VAR>ComplementedLattice α<VAR>h : IsAtomic α<GOAL>IsStronglyCoatomic α
<VAR>α : Type u_2<VAR>Lattice α<VAR>BoundedOrder α<VAR>IsModularLattice α<VAR>ComplementedLattice α<VAR>h : IsCoatomic α<GOAL>IsStronglyAtomic α
<VAR>p : Prop<GOAL>IsAtom p ↔ p
<VAR>p : Prop<GOAL>IsCoatom p ↔ ¬p
<VAR>ι : Type u_4<VAR>π : ι → Type u<VAR>(i : ι) → Bot (π i)<VAR>f : (i : ι) → π i<GOAL>f = ⊥ ↔ ∀ (i : ι), f i = ⊥
<VAR>ι : Type u_4<VAR>π : ι → Type u<VAR>f : (i : ι) → π i<VAR>(i : ι) → PartialOrder (π i)<VAR>(i : ι) → OrderBot (π i)<GOAL>IsAtom f ↔ ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥
<VAR>ι : Type u_4<VAR>π : ι → Type u<VAR>i : ι<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (π i)<VAR>(i : ι) → OrderBot (π i)<VAR>a : π i<VAR>h : IsAtom a<GOAL>IsAtom (Function.update ⊥ i a)
<VAR>ι : Type u_4<VAR>π : ι → Type u<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (π i)<VAR>(i : ι) → OrderBot (π i)<VAR>f : (i : ι) → π i<GOAL>IsAtom f ↔ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a : α<GOAL>IsAtom aᶜ ↔ IsCoatom a
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a : α<GOAL>IsCoatom aᶜ ↔ IsAtom a
<VAR>α : Type u_2<VAR>x : α<GOAL>IsAtom {x}
<VAR>α : Type u_2<VAR>s : Set α<GOAL>IsAtom s ↔ ∃ x, s = {x}
<VAR>α : Type u_2<VAR>s : Set α<GOAL>IsCoatom s ↔ ∃ x, s = {x}ᶜ
<VAR>α : Type u_2<VAR>x : α<GOAL>IsCoatom {x}ᶜ
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>h : Monovary f g<VAR>s : Set ι<GOAL>MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>h : Antivary f g<VAR>s : Set ι<GOAL>AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>MonovaryOn f g ∅
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>AntivaryOn f g ∅
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>MonovaryOn f g Set.univ ↔ Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>AntivaryOn f g Set.univ ↔ Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s t : Set ι<VAR>hst : s ⊆ t<VAR>h : MonovaryOn f g t<GOAL>MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s t : Set ι<VAR>hst : s ⊆ t<VAR>h : AntivaryOn f g t<GOAL>AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>g : ι → β<VAR>a : α<GOAL>Monovary (Function.const ι a) g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>g : ι → β<VAR>a : α<GOAL>Antivary (Function.const ι a) g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>b : β<GOAL>Monovary f (Function.const ι b)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>b : β<GOAL>Antivary f (Function.const ι b)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>Preorder α<VAR>f : ι → α<GOAL>Monovary f f
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>Preorder α<VAR>f : ι → α<VAR>s : Set ι<GOAL>MonovaryOn f f s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Subsingleton ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Subsingleton ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Subsingleton ι<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Subsingleton ι<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>g : ι → β<VAR>a : α<VAR>s : Set ι<GOAL>MonovaryOn (Function.const ι a) g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>g : ι → β<VAR>a : α<VAR>s : Set ι<GOAL>AntivaryOn (Function.const ι a) g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>b : β<VAR>s : Set ι<GOAL>MonovaryOn f (Function.const ι b) s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>b : β<VAR>s : Set ι<GOAL>AntivaryOn f (Function.const ι b) s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>h : Monovary f g<VAR>k : ι' → ι<GOAL>Monovary (f ∘ k) (g ∘ k)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>h : Antivary f g<VAR>k : ι' → ι<GOAL>Antivary (f ∘ k) (g ∘ k)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>h : MonovaryOn f g s<VAR>k : ι' → ι<GOAL>MonovaryOn (f ∘ k) (g ∘ k) (k ⁻¹' s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>h : AntivaryOn f g s<VAR>k : ι' → ι<GOAL>AntivaryOn (f ∘ k) (g ∘ k) (k ⁻¹' s)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : ι → α<VAR>f' : α → γ<VAR>g : ι → β<VAR>h : Monovary f g<VAR>hf : Monotone f'<GOAL>Monovary (f' ∘ f) g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : ι → α<VAR>f' : α → γ<VAR>g : ι → β<VAR>h : Monovary f g<VAR>hf : Antitone f'<GOAL>Antivary (f' ∘ f) g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : ι → α<VAR>f' : α → γ<VAR>g : ι → β<VAR>h : Antivary f g<VAR>hf : Monotone f'<GOAL>Antivary (f' ∘ f) g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : ι → α<VAR>f' : α → γ<VAR>g : ι → β<VAR>h : Antivary f g<VAR>hf : Antitone f'<GOAL>Monovary (f' ∘ f) g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : ι → α<VAR>f' : α → γ<VAR>g : ι → β<VAR>s : Set ι<VAR>h : MonovaryOn f g s<VAR>hf : Monotone f'<GOAL>MonovaryOn (f' ∘ f) g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : ι → α<VAR>f' : α → γ<VAR>g : ι → β<VAR>s : Set ι<VAR>h : MonovaryOn f g s<VAR>hf : Antitone f'<GOAL>AntivaryOn (f' ∘ f) g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : ι → α<VAR>f' : α → γ<VAR>g : ι → β<VAR>s : Set ι<VAR>h : AntivaryOn f g s<VAR>hf : Monotone f'<GOAL>AntivaryOn (f' ∘ f) g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : ι → α<VAR>f' : α → γ<VAR>g : ι → β<VAR>s : Set ι<VAR>h : AntivaryOn f g s<VAR>hf : Antitone f'<GOAL>MonovaryOn (f' ∘ f) g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary f g → Monovary (⇑OrderDual.toDual ∘ f) (⇑OrderDual.toDual ∘ g)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary f g → Antivary (⇑OrderDual.toDual ∘ f) (⇑OrderDual.toDual ∘ g)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary f g → Antivary (⇑OrderDual.toDual ∘ f) g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary f g → Monovary (⇑OrderDual.toDual ∘ f) g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary f g → Antivary f (⇑OrderDual.toDual ∘ g)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary f g → Monovary f (⇑OrderDual.toDual ∘ g)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>MonovaryOn f g s → MonovaryOn (⇑OrderDual.toDual ∘ f) (⇑OrderDual.toDual ∘ g) s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>AntivaryOn f g s → AntivaryOn (⇑OrderDual.toDual ∘ f) (⇑OrderDual.toDual ∘ g) s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>MonovaryOn f g s → AntivaryOn (⇑OrderDual.toDual ∘ f) g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>AntivaryOn f g s → MonovaryOn (⇑OrderDual.toDual ∘ f) g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>MonovaryOn f g s → AntivaryOn f (⇑OrderDual.toDual ∘ g) s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>AntivaryOn f g s → MonovaryOn f (⇑OrderDual.toDual ∘ g) s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary (⇑OrderDual.toDual ∘ f) g ↔ Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary f (⇑OrderDual.toDual ∘ g) ↔ Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary (⇑OrderDual.toDual ∘ f) g ↔ Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary f (⇑OrderDual.toDual ∘ g) ↔ Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>MonovaryOn (⇑OrderDual.toDual ∘ f) g s ↔ AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>MonovaryOn f (⇑OrderDual.toDual ∘ g) s ↔ AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>AntivaryOn (⇑OrderDual.toDual ∘ f) g s ↔ MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>AntivaryOn f (⇑OrderDual.toDual ∘ g) s ↔ MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>Preorder α<VAR>f : ι → α<VAR>PartialOrder ι<GOAL>Monovary f id ↔ Monotone f
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>Preorder α<VAR>f : ι → α<VAR>PartialOrder ι<GOAL>Antivary f id ↔ Antitone f
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>Preorder α<VAR>f : ι → α<VAR>s : Set ι<VAR>PartialOrder ι<GOAL>MonovaryOn f id s ↔ MonotoneOn f s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>Preorder α<VAR>f : ι → α<VAR>s : Set ι<VAR>PartialOrder ι<GOAL>AntivaryOn f id s ↔ AntitoneOn f s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>LinearOrder ι<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>LinearOrder ι<VAR>hf : Monotone f<VAR>hg : Antitone g<GOAL>Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>LinearOrder ι<VAR>hf : Antitone f<VAR>hg : Antitone g<GOAL>Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>LinearOrder ι<VAR>hf : Antitone f<VAR>hg : Monotone g<GOAL>Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>LinearOrder ι<VAR>hf : MonotoneOn f s<VAR>hg : MonotoneOn g s<GOAL>MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>LinearOrder ι<VAR>hf : MonotoneOn f s<VAR>hg : AntitoneOn g s<GOAL>AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>LinearOrder ι<VAR>hf : AntitoneOn f s<VAR>hg : AntitoneOn g s<GOAL>MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>LinearOrder ι<VAR>hf : AntitoneOn f s<VAR>hg : MonotoneOn g s<GOAL>AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>LinearOrder β<VAR>Preorder γ<VAR>f : ι → α<VAR>g : ι → β<VAR>g' : β → γ<VAR>s : Set ι<VAR>h : MonovaryOn f g s<VAR>hg : MonotoneOn g' (g '' s)<GOAL>MonovaryOn f (g' ∘ g) s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>LinearOrder β<VAR>Preorder γ<VAR>f : ι → α<VAR>g : ι → β<VAR>g' : β → γ<VAR>s : Set ι<VAR>h : MonovaryOn f g s<VAR>hg : AntitoneOn g' (g '' s)<GOAL>AntivaryOn f (g' ∘ g) s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>LinearOrder β<VAR>Preorder γ<VAR>f : ι → α<VAR>g : ι → β<VAR>g' : β → γ<VAR>s : Set ι<VAR>h : AntivaryOn f g s<VAR>hg : MonotoneOn g' (g '' s)<GOAL>AntivaryOn f (g' ∘ g) s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>LinearOrder β<VAR>Preorder γ<VAR>f : ι → α<VAR>g : ι → β<VAR>g' : β → γ<VAR>s : Set ι<VAR>h : AntivaryOn f g s<VAR>hg : AntitoneOn g' (g '' s)<GOAL>MonovaryOn f (g' ∘ g) s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>LinearOrder β<VAR>f : ι → α<VAR>g : ι → β<VAR>h : Monovary f g<GOAL>Monovary g f
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>LinearOrder β<VAR>f : ι → α<VAR>g : ι → β<VAR>h : Antivary f g<GOAL>Antivary g f
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>LinearOrder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>h : MonovaryOn f g s<GOAL>MonovaryOn g f s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>LinearOrder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>h : AntivaryOn f g s<GOAL>AntivaryOn g f s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary f g ↔ Monovary g f
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary f g ↔ Antivary g f
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>MonovaryOn f g s ↔ MonovaryOn g f s
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>AntivaryOn f g s ↔ AntivaryOn g f s
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>IsSimpleOrder α<VAR>DecidableEq α<GOAL>Finset.univ = {⊤, ⊥}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>IsSimpleOrder α<VAR>DecidableEq α<GOAL>Fintype.card α = 2
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<VAR>IsStronglyAtomic α<VAR>ha : (Set.Ici a).Infinite<VAR>hfin : {x | a ⋖ x}.Finite<GOAL>∃ b, a ⋖ b ∧ (Set.Ici b).Infinite
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<VAR>IsStronglyCoatomic α<VAR>ha : (Set.Iic a).Infinite<VAR>hfin : {x | x ⋖ a}.Finite<GOAL>∃ b, b ⋖ a ∧ (Set.Iic b).Infinite
<VAR>a b : ℕ<GOAL>Finset.Icc a b = { val := ↑(List.range' a (b + 1 - a)), nodup := ⋯ }
<VAR>a b : ℕ<GOAL>Finset.Ico a b = { val := ↑(List.range' a (b - a)), nodup := ⋯ }
<VAR>a b : ℕ<GOAL>Finset.Ioc a b = { val := ↑(List.range' (a + 1) (b - a)), nodup := ⋯ }
<VAR>a b : ℕ<GOAL>Finset.Ioo a b = { val := ↑(List.range' (a + 1) (b - a - 1)), nodup := ⋯ }