43 lines
1.8 KiB
Plaintext
43 lines
1.8 KiB
Plaintext
/--
|
||
@[ext] structure Cut where
|
||
S : Set ℚ
|
||
|
||
not_all : S ≠ Set.univ
|
||
nonempty : S.Nonempty
|
||
|
||
lt_elem x y : x ∈ S → y < x → y ∈ S
|
||
no_max x : x ∈ S → ∃ y ∈ S, x < y
|
||
--/
|
||
|
||
-- structure == inductive, but structure has one constructor. it is all these things it's an and, it's like a named tuple or record in coq, structs in C
|
||
structure Cut where
|
||
carrier: Set ℚ -- carrier == α in Rudin, the actual cut
|
||
not_empty: carrier ≠ {} -- α ≠ ∅ (I)
|
||
not_all: carrier ≠ Set.univ -- alpha ≠ Set ℚ, carrier ≠ { _a | True} (I)
|
||
p_less_q_in_carrier: ∀ p ∈ carrier, ∀ q : ℚ, q < p -> q ∈ carrier -- (II)
|
||
p_less_q_in_carrier': (p : ℚ) -> p ∈ carrier -> (q : ℚ) -> q < p -> q ∈ carrier -- (III)
|
||
always_exist_a_larger_element: ∀ p ∈ carrier, ∃ r ∈ carrier, p < r -- (III')
|
||
if_q_not_in_carrier_then_grater_than_elem_in_carrier: ∀ p ∈ carrier, ∀ q : ℚ, (q ∉ carrier) → p < q
|
||
|
||
-- Now let's debug/test the above structure we defined
|
||
-- 1. let's proof some subset of Q is a (Dedikin) Cut
|
||
-- 2. thm, rfl proof of that p_less_q_in_carrier' == p_less_q_in_carrier'
|
||
-- 3. continue in Rudin!
|
||
-- 4. Show (II) implies --> (IV) & (V)
|
||
|
||
def A : Set ℚ := { x | x < 3}
|
||
theorem A_is_a_cut : Cut d
|
||
{
|
||
carrier := A,
|
||
not_empty := sorry, -- Proof that A is not empty
|
||
not_all := sorry, -- Proof that A is not the set of all rationals
|
||
p_less_q_in_carrier := sorry, -- Proof of ∀ p ∈ A, ∀ q : ℚ, q < p -> q ∈ A
|
||
p_less_q_in_carrier' := sorry, -- Alternative proof of the same property
|
||
always_exist_a_larger_element := sorry, -- Proof of ∀ p ∈ A, ∃ r ∈ A, p < r
|
||
if_q_not_in_carrier_then_grater_than_elem_in_carrier := sorry -- Proof of ∀ p ∈ A, ∀ q : ℚ, (q ∉ A) → p < q
|
||
}
|
||
|
||
/--
|
||
include private proofs discussed with scott
|
||
--/
|