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))

Created: