The Theory orders
 Parents
 sets
 Children
 equiv_rel ℝ
 Constants
 Irrefl 'a SET × ('a → 'a → BOOL) → BOOL Antisym 'a SET × ('a → 'a → BOOL) → BOOL Trans 'a SET × ('a → 'a → BOOL) → BOOL StrictPartialOrder 'a SET × ('a → 'a → BOOL) → BOOL Trich 'a SET × ('a → 'a → BOOL) → BOOL StrictLinearOrder 'a SET × ('a → 'a → BOOL) → BOOL \$DenseIn 'a SET → 'a SET × ('a → 'a → BOOL) → BOOL Dense 'a SET × ('a → 'a → BOOL) → BOOL UpperBound 'a SET × ('a → 'a → BOOL) × 'a → BOOL \$HasSupremum 'a SET → 'a × 'a SET × ('a → 'a → BOOL) → BOOL UnboundedAbove 'a SET × ('a → 'a → BOOL) → BOOL UnboundedBelow 'a SET × ('a → 'a → BOOL) → BOOL Complete 'a SET × ('a → 'a → BOOL) → BOOL Cuts 'a SET × ('a → 'a → BOOL) → 'a SET SET DownSet 'a SET × ('a → 'a → BOOL) × 'a → 'a SET DownSets 'a SET × ('a → 'a → BOOL) × 'a SET → 'a SET SET
 Fixity
 Right Infix 210: DenseIn HasSupremum << <<<
 Definitions
 Irrefl ⊢ ∀ X \$<<• Irrefl (X, \$<<) ⇔ (∀ x• x ∈ X ⇒ ¬ x << x) Antisym ⊢ ∀ X \$<< • Antisym (X, \$<<) ⇔ (∀ x y • x ∈ X ∧ y ∈ X ∧ ¬ x = y ⇒ ¬ (x << y ∧ y << x)) Trans ⊢ ∀ X \$<< • Trans (X, \$<<) ⇔ (∀ x y z • x ∈ X ∧ y ∈ X ∧ z ∈ X ∧ x << y ∧ y << z ⇒ x << z) StrictPartialOrder ⊢ ∀ X \$<< • StrictPartialOrder (X, \$<<) ⇔ Irrefl (X, \$<<) ∧ Antisym (X, \$<<) ∧ Trans (X, \$<<) Trich ⊢ ∀ X \$<< • Trich (X, \$<<) ⇔ (∀ x y • x ∈ X ∧ y ∈ X ∧ ¬ x = y ⇒ x << y ∨ y << x) StrictLinearOrder ⊢ ∀ X \$<< • StrictLinearOrder (X, \$<<) ⇔ StrictPartialOrder (X, \$<<) ∧ Trich (X, \$<<) DenseIn ⊢ ∀ A X \$<< • A DenseIn (X, \$<<) ⇔ (∀ x y • x ∈ X ∧ y ∈ X ∧ x << y ⇒ (∃ a• a ∈ A ∧ x << a ∧ a << y)) Dense ⊢ ∀ X \$<<• Dense (X, \$<<) ⇔ X DenseIn (X, \$<<) UpperBound ⊢ ∀ A \$<< x • UpperBound (A, \$<<, x) ⇔ (∀ a• a ∈ A ⇒ a << x) HasSupremum ⊢ ∀ A \$<< x X • A HasSupremum (x, X, \$<<) ⇔ UpperBound (A, \$<<, x) ∧ (∀ y • y ∈ X ∧ UpperBound (A, \$<<, y) ⇒ ¬ y << x) UnboundedAbove ⊢ ∀ A \$<< • UnboundedAbove (A, \$<<) ⇔ (∀ b• b ∈ A ⇒ (∃ c• c ∈ A ∧ b << c)) UnboundedBelow ⊢ ∀ A \$<< • UnboundedBelow (A, \$<<) ⇔ (∀ b• b ∈ A ⇒ (∃ c• c ∈ A ∧ c << b)) Complete ⊢ ∀ X \$<< • Complete (X, \$<<) ⇔ (∀ A x • ¬ A = {} ∧ A ⊆ X ∧ UnboundedAbove (A, \$<<) ∧ x ∈ X ∧ UpperBound (A, \$<<, x) ⇒ (∃ y• y ∈ X ∧ A HasSupremum (y, X, \$<<))) Cuts ⊢ ∀ X \$<< A • A ∈ Cuts (X, \$<<) ⇔ A ⊆ X ∧ ¬ A = {} ∧ UnboundedAbove (A, \$<<) ∧ (∃ x• x ∈ X ∧ UpperBound (A, \$<<, x)) ∧ (∀ a b• a ∈ A ∧ b ∈ X ∧ b << a ⇒ b ∈ A) DownSet ⊢ ∀ X \$<< x• DownSet (X, \$<<, x) = {y|y ∈ X ∧ y << x} DownSets ⊢ ∀ X \$<< A s • s ∈ DownSets (X, \$<<, A) ⇔ (∃ x• x ∈ A ∧ s = DownSet (X, \$<<, x))
 Theorems
 ⊂_irrefl_thm ⊢ ∀ V• Irrefl (V, \$⊂) ⊂_antisym_thm ⊢ ∀ V• Antisym (V, \$⊂) ⊂_trans_thm ⊢ ∀ V• Trans (V, \$⊂) cuts_trich_thm ⊢ ∀ X \$<< • Trans (X, \$<<) ∧ Trich (X, \$<<) ⇒ Trich (Cuts (X, \$<<), \$⊂) cuts_strict_partial_order_thm ⊢ ∀ X \$<<• StrictPartialOrder (Cuts (X, \$<<), \$⊂) cuts_strict_linear_order_thm ⊢ ∀ X \$<< • StrictLinearOrder (X, \$<<) ⇒ StrictLinearOrder (Cuts (X, \$<<), \$⊂) cuts_complete_thm ⊢ ∀ X \$<<• Complete (Cuts (X, \$<<), \$⊂) down_sets_cuts_thm ⊢ ∀ X \$<< A • A ⊆ X ∧ Irrefl (X, \$<<) ∧ Trans (X, \$<<) ∧ UnboundedBelow (A, \$<<) ∧ A DenseIn (X, \$<<) ⇒ DownSets (X, \$<<, A) ⊆ Cuts (X, \$<<) down_sets_dense_thm ⊢ ∀ X \$<< A • A ⊆ X ∧ StrictLinearOrder (X, \$<<) ∧ UnboundedBelow (A, \$<<) ∧ A DenseIn (X, \$<<) ⇒ DownSets (X, \$<<, A) DenseIn (Cuts (X, \$<<), \$⊂) dense_superset_thm ⊢ ∀ X \$<< A B • A ⊆ B ∧ B ⊆ X ∧ A DenseIn (X, \$<<) ⇒ B DenseIn (X, \$<<) dense_universe_thm ⊢ ∀ X \$<< A • A ⊆ X ∧ A DenseIn (X, \$<<) ⇒ Dense (X, \$<<) downset_cut_thm ⊢ ∀ X \$<< a • a ∈ X ∧ Trans (X, \$<<) ∧ UnboundedBelow (X, \$<<) ∧ X DenseIn (X, \$<<) ⇒ DownSet (X, \$<<, a) ∈ Cuts (X, \$<<) down_sets_less_thm ⊢ ∀ X \$<< a b • a ∈ X ∧ b ∈ X ∧ StrictLinearOrder (X, \$<<) ⇒ (DownSet (X, \$<<, a) ⊂ DownSet (X, \$<<, b) ⇔ a << b) cuts_unbounded_above_thm ⊢ ∀ X \$<< • Irrefl (X, \$<<) ∧ Trans (X, \$<<) ∧ UnboundedAbove (X, \$<<) ∧ X DenseIn (X, \$<<) ⇒ UnboundedAbove (Cuts (X, \$<<), \$⊂) cuts_unbounded_below_thm ⊢ ∀ X \$<< • Irrefl (X, \$<<) ∧ Trans (X, \$<<) ∧ UnboundedBelow (X, \$<<) ∧ X DenseIn (X, \$<<) ⇒ UnboundedBelow (Cuts (X, \$<<), \$⊂) dense_complete_subset_thm ⊢ ∀ X \$<< A • StrictLinearOrder (X, \$<<) ∧ A ⊆ X ∧ UnboundedAbove (X, \$<<) ∧ UnboundedBelow (X, \$<<) ∧ A DenseIn (X, \$<<) ∧ Complete (A, \$<<) ⇒ A = X induced_order_irrefl_thm ⊢ ∀ X \$<< f • (∀ a• f a ∈ X) ∧ Irrefl (X, \$<<) ⇒ Irrefl (Universe, (λ a b• f a << f b)) induced_order_antisym_thm ⊢ ∀ X \$<< f • (∀ a• f a ∈ X) ∧ Irrefl (X, \$<<) ∧ Antisym (X, \$<<) ⇒ Antisym (Universe, (λ a b• f a << f b)) induced_order_trans_thm ⊢ ∀ X \$<< f • (∀ a• f a ∈ X) ∧ Trans (X, \$<<) ⇒ Trans (Universe, (λ a b• f a << f b)) induced_order_trich_thm ⊢ ∀ X \$<< f • (∀ a• f a ∈ X) ∧ OneOne f ∧ Trich (X, \$<<) ⇒ Trich (Universe, (λ a b• f a << f b)) induced_strict_partial_order_thm ⊢ ∀ X \$<< f • (∀ a• f a ∈ X) ∧ StrictPartialOrder (X, \$<<) ⇒ StrictPartialOrder (Universe, (λ a b• f a << f b)) induced_strict_linear_order_thm ⊢ ∀ X \$<< f • (∀ a• f a ∈ X) ∧ OneOne f ∧ StrictLinearOrder (X, \$<<) ⇒ StrictLinearOrder (Universe, (λ a b• f a << f b)) induced_order_complete_thm ⊢ ∀ X \$<< f • (∀ a• f a ∈ X) ∧ OneOne f ∧ (∀ x• x ∈ X ⇒ (∃ a• x = f a)) ∧ Complete (X, \$<<) ⇒ Complete (Universe, (λ a b• f a << f b)) induced_order_dense_thm ⊢ ∀ X \$<< f A • (∀ a• f a ∈ X) ∧ OneOne f ∧ (∀ x• x ∈ X ⇒ (∃ a• x = f a)) ∧ {x|∃ a• a ∈ A ∧ x = f a} DenseIn (X, \$<<) ⇒ A DenseIn (Universe, (λ a b• f a << f b)) induced_order_unbounded_above_thm ⊢ ∀ X \$<< f • (∀ a• f a ∈ X) ∧ OneOne f ∧ (∀ x• x ∈ X ⇒ (∃ a• x = f a)) ∧ UnboundedAbove (X, \$<<) ⇒ UnboundedAbove (Universe, (λ a b• f a << f b)) induced_order_unbounded_below_thm ⊢ ∀ X \$<< f • (∀ a• f a ∈ X) ∧ OneOne f ∧ (∀ x• x ∈ X ⇒ (∃ a• x = f a)) ∧ UnboundedBelow (X, \$<<) ⇒ UnboundedBelow (Universe, (λ a b• f a << f b))