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 $<<
fill• Antisym (X, $<<)
fill⇔ (∀ x y
fill• x ∈ X ∧ y ∈ X ∧ ¬ x = y ⇒ ¬ (x << y ∧ y << x))
Trans
⊢ ∀ X $<<
fill• Trans (X, $<<)
fill⇔ (∀ x y z
fill• x ∈ X ∧ y ∈ X ∧ z ∈ X ∧ x << y ∧ y << z
fill⇒ x << z)
StrictPartialOrder
⊢ ∀ X $<<
fill• StrictPartialOrder (X, $<<)
fill⇔ Irrefl (X, $<<)
fill∧ Antisym (X, $<<)
fill∧ Trans (X, $<<)
Trich
⊢ ∀ X $<<
fill• Trich (X, $<<)
fill⇔ (∀ x y
fill• x ∈ X ∧ y ∈ X ∧ ¬ x = y ⇒ x << y ∨ y << x)
StrictLinearOrder
⊢ ∀ X $<<
fill• StrictLinearOrder (X, $<<)
fill⇔ StrictPartialOrder (X, $<<) ∧ Trich (X, $<<)
DenseIn
⊢ ∀ A X $<<
fill• A DenseIn (X, $<<)
fill⇔ (∀ x y
fill• x ∈ X ∧ y ∈ X ∧ x << y
fill⇒ (∃ a• a ∈ A ∧ x << a ∧ a << y))
Dense
⊢ ∀ X $<<• Dense (X, $<<) ⇔ X DenseIn (X, $<<)
UpperBound
⊢ ∀ A $<< x
fill• UpperBound (A, $<<, x) ⇔ (∀ a• a ∈ A ⇒ a << x)
HasSupremum
⊢ ∀ A $<< x X
fill• A HasSupremum (x, X, $<<)
fill⇔ UpperBound (A, $<<, x)
fill∧ (∀ y
fill• y ∈ X ∧ UpperBound (A, $<<, y) ⇒ ¬ y << x)
UnboundedAbove
⊢ ∀ A $<<
fill• UnboundedAbove (A, $<<)
fill⇔ (∀ b• b ∈ A ⇒ (∃ c• c ∈ A ∧ b << c))
UnboundedBelow
⊢ ∀ A $<<
fill• UnboundedBelow (A, $<<)
fill⇔ (∀ b• b ∈ A ⇒ (∃ c• c ∈ A ∧ c << b))
Complete
⊢ ∀ X $<<
fill• Complete (X, $<<)
fill⇔ (∀ A x
fill• ¬ A = {}
fill∧ A ⊆ X
fill∧ UnboundedAbove (A, $<<)
fill∧ x ∈ X
fill∧ UpperBound (A, $<<, x)
fill⇒ (∃ y• y ∈ X ∧ A HasSupremum (y, X, $<<)))
Cuts
⊢ ∀ X $<< A
fill• A ∈ Cuts (X, $<<)
fill⇔ A ⊆ X
fill∧ ¬ A = {}
fill∧ UnboundedAbove (A, $<<)
fill∧ (∃ x• x ∈ X ∧ UpperBound (A, $<<, x))
fill∧ (∀ 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
fill• s ∈ DownSets (X, $<<, A)
fill⇔ (∃ 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 $<<
fill• Trans (X, $<<) ∧ Trich (X, $<<)
fill⇒ Trich (Cuts (X, $<<), $⊂)
cuts_strict_partial_order_thm
⊢ ∀ X $<<• StrictPartialOrder (Cuts (X, $<<), $⊂)
cuts_strict_linear_order_thm
⊢ ∀ X $<<
fill• StrictLinearOrder (X, $<<)
fill⇒ StrictLinearOrder (Cuts (X, $<<), $⊂)
cuts_complete_thm
⊢ ∀ X $<<• Complete (Cuts (X, $<<), $⊂)
down_sets_cuts_thm
⊢ ∀ X $<< A
fill• A ⊆ X
fill∧ Irrefl (X, $<<)
fill∧ Trans (X, $<<)
fill∧ UnboundedBelow (A, $<<)
fill∧ A DenseIn (X, $<<)
fill⇒ DownSets (X, $<<, A) ⊆ Cuts (X, $<<)
down_sets_dense_thm
⊢ ∀ X $<< A
fill• A ⊆ X
fill∧ StrictLinearOrder (X, $<<)
fill∧ UnboundedBelow (A, $<<)
fill∧ A DenseIn (X, $<<)
fill⇒ DownSets (X, $<<, A)
fillDenseIn (Cuts (X, $<<), $⊂)
dense_superset_thm
⊢ ∀ X $<< A B
fill• A ⊆ B ∧ B ⊆ X ∧ A DenseIn (X, $<<)
fill⇒ B DenseIn (X, $<<)
dense_universe_thm
⊢ ∀ X $<< A
fill• A ⊆ X ∧ A DenseIn (X, $<<) ⇒ Dense (X, $<<)
downset_cut_thm
⊢ ∀ X $<< a
fill• a ∈ X
fill∧ Trans (X, $<<)
fill∧ UnboundedBelow (X, $<<)
fill∧ X DenseIn (X, $<<)
fill⇒ DownSet (X, $<<, a) ∈ Cuts (X, $<<)
down_sets_less_thm
⊢ ∀ X $<< a b
fill• a ∈ X ∧ b ∈ X ∧ StrictLinearOrder (X, $<<)
fill⇒ (DownSet (X, $<<, a) ⊂ DownSet (X, $<<, b)
fill⇔ a << b)
cuts_unbounded_above_thm
⊢ ∀ X $<<
fill• Irrefl (X, $<<)
fill∧ Trans (X, $<<)
fill∧ UnboundedAbove (X, $<<)
fill∧ X DenseIn (X, $<<)
fill⇒ UnboundedAbove (Cuts (X, $<<), $⊂)
cuts_unbounded_below_thm
⊢ ∀ X $<<
fill• Irrefl (X, $<<)
fill∧ Trans (X, $<<)
fill∧ UnboundedBelow (X, $<<)
fill∧ X DenseIn (X, $<<)
fill⇒ UnboundedBelow (Cuts (X, $<<), $⊂)
dense_complete_subset_thm
⊢ ∀ X $<< A
fill• StrictLinearOrder (X, $<<)
fill∧ A ⊆ X
fill∧ UnboundedAbove (X, $<<)
fill∧ UnboundedBelow (X, $<<)
fill∧ A DenseIn (X, $<<)
fill∧ Complete (A, $<<)
fill⇒ A = X
induced_order_irrefl_thm
⊢ ∀ X $<< f
fill• (∀ a• f a ∈ X) ∧ Irrefl (X, $<<)
fill⇒ Irrefl (Universe, (λ a b• f a << f b))
induced_order_antisym_thm
⊢ ∀ X $<< f
fill• (∀ a• f a ∈ X) ∧ Irrefl (X, $<<) ∧ Antisym (X, $<<)
fill⇒ Antisym (Universe, (λ a b• f a << f b))
induced_order_trans_thm
⊢ ∀ X $<< f
fill• (∀ a• f a ∈ X) ∧ Trans (X, $<<)
fill⇒ Trans (Universe, (λ a b• f a << f b))
induced_order_trich_thm
⊢ ∀ X $<< f
fill• (∀ a• f a ∈ X) ∧ OneOne f ∧ Trich (X, $<<)
fill⇒ Trich (Universe, (λ a b• f a << f b))
induced_strict_partial_order_thm
⊢ ∀ X $<< f
fill• (∀ a• f a ∈ X) ∧ StrictPartialOrder (X, $<<)
fill⇒ StrictPartialOrder
fill(Universe, (λ a b• f a << f b))
induced_strict_linear_order_thm
⊢ ∀ X $<< f
fill• (∀ a• f a ∈ X)
fill∧ OneOne f
fill∧ StrictLinearOrder (X, $<<)
fill⇒ StrictLinearOrder
fill(Universe, (λ a b• f a << f b))
induced_order_complete_thm
⊢ ∀ X $<< f
fill• (∀ a• f a ∈ X)
fill∧ OneOne f
fill∧ (∀ x• x ∈ X ⇒ (∃ a• x = f a))
fill∧ Complete (X, $<<)
fill⇒ Complete (Universe, (λ a b• f a << f b))
induced_order_dense_thm
⊢ ∀ X $<< f A
fill• (∀ a• f a ∈ X)
fill∧ OneOne f
fill∧ (∀ x• x ∈ X ⇒ (∃ a• x = f a))
fill∧ {x|∃ a• a ∈ A ∧ x = f a} DenseIn (X, $<<)
fill⇒ A DenseIn (Universe, (λ a b• f a << f b))
induced_order_unbounded_above_thm
⊢ ∀ X $<< f
fill• (∀ a• f a ∈ X)
fill∧ OneOne f
fill∧ (∀ x• x ∈ X ⇒ (∃ a• x = f a))
fill∧ UnboundedAbove (X, $<<)
fill⇒ UnboundedAbove (Universe, (λ a b• f a << f b))
induced_order_unbounded_below_thm
⊢ ∀ X $<< f
fill• (∀ a• f a ∈ X)
fill∧ OneOne f
fill∧ (∀ x• x ∈ X ⇒ (∃ a• x = f a))
fill∧ UnboundedBelow (X, $<<)
fill⇒ UnboundedBelow (Universe, (λ a b• f a << f b))

up quick index

privacy policy

Created:

V