New Reward Bounties (Dieudonne, Reals)

by BlakeKeiller, Sunday, February 07, 2021, 16:12 (301 days ago) @ BlakeKeiller

Dieudonne_2_2_3a : TMJzRJ8FUbafjnkpD76W33XD5VbGxuYNL9o
forall A c= R, finite A -> exists a :e A, forall x :e A, a <= x.

Dieudonne_2_2_3b : TMQy9tPL9pyAKAHAAaTFHfyY7nHZFXD8f4h
forall A c= R, finite A -> exists b :e A, forall x :e A, x <= b.

Dieudonne_2_2_5a : TMM6ay3f6U1nfvLBiDPz1sq2dHWxX7SdV4B
forall n :e omega, forall x y :e R :^: n, (forall i :e n, x i <= y i) -> finseqsum n x <= finseqsum n y.

Dieudonne_2_2_5b : TMce47Gcyw4Dmk9EuVb5nytGXoGZJLCYVLU
forall n :e omega, forall x y :e R :^: n, (forall i :e n, x i <= y i) -> (exists i :e n, x i < y i) -> finseqsum n x < finseqsum n y.

Dieudonne_2_2_6 : TMdZxf1WiBt1hZTNG2KfAE4RGCYBfX5b6YE
forall x y z :e R, x <= y <-> x + z <= y + z.

Dieudonne_2_2_7e : TMMV3gE1eKPX49sr7atFfzx8pAxwxmwav9U
forall x y :e R, x <= y -> - y <= - x.

Dieudonne_2_2_7f : TMV3dr1Xxf3SHi14vqzh6tgtYqt2aqWiv8n
forall x y :e R, - y <= - x -> x <= y.

Dieudonne_2_2_8a : TMP1aTMo25AUers6ipDNW8Bevvosd9qhHrk
forall n :e omega, forall x :e R :^: n, (forall i :e n, zero <= x i) -> zero <= finseqsum n x.

Dieudonne_2_2_8b : TMcfjCBjiKJGEj2nDB29cNxRsCrLzxoVcHQ
forall n :e omega, forall x :e R :^: n, (forall i :e n, zero <= x i) -> finseqsum n x = zero -> forall i :e n, x i = zero.

Dieudonne_2_2_9a : TMQ16vrLBKAtFyaZjJKu3EaveZEdn9iEqN8
forall a :e R, zero < a -> forall x :e R, abs x <= a -> - a <= x /\ x <= a.

Dieudonne_2_2_9b : TMNz4JKodQQhxK18Xzk2NiHGsLGqmMhPwEZ
forall a :e R, zero < a -> forall x :e R, - a <= x -> x <= a -> abs x <= a.

Dieudonne_2_2_9c : TMJANcfGFWwFCuwg8ZzAj98yiMyhJM1yyex
forall a :e R, zero < a -> forall x :e R, abs x < a -> - a < x /\ x < a.

Dieudonne_2_2_9d : TMTHzysQZQLA7ZWfPgbaWXMewgThCgHQehG
forall a :e R, zero < a -> forall x :e R, - a < x -> x < a -> abs x < a.

Dieudonne_2_2_10a : TMQhGKHizkQ9pD6VjNAsUfRAijpGeHoHXBj
forall x y :e R, abs (x + y) <= abs x + abs y.

Dieudonne_2_2_10b : TMJKrzLhYYrNEABZxvMdAewkPxdfWgrGmaL
forall x y :e R, abs (abs x + - abs y) <= abs (x + - y).

Dieudonne_2_2_11 : TMZwaC2JBBy7cjfkLcLMkDiAje7Qbq2RRSH
forall z :e R, zero <= z -> forall x y :e R, x <= y -> x * z <= y * z.

Dieudonne_2_2_12a : TMcUVZsFboifsYmhgqKVtErtBdFcKiLMhSt
forall x y :e R, x <= zero -> zero <= y -> x * y <= zero.

Dieudonne_2_2_12b : TMSDLuJFRvFVN1qvAvcauzojpJq9K5sGQQt
forall x y :e R, x <= zero -> y <= zero -> zero <= x * y.

Dieudonne_2_2_12c : TMVwP5my7BcDMtYgHNRfVWgYKW1FE7JSenM
forall x y :e R, x < zero -> zero < y -> x * y < zero.

Dieudonne_2_2_12d : TMJ2ezJwVaL7xjuLPv43YkH9Z6pEofFXBM1
forall x y :e R, x < zero -> y < zero -> zero < x * y.

Dieudonne_2_2_13a : TMcA1PyGZynxg92qnswas1QUUAYLo3Aj1Sp
forall x :e R, zero < x -> zero < one :/: x.

Dieudonne_2_2_13b : TMU4TC4gsQqWnNo1wLet97Fsff2TCgnQ8GM
forall z :e R, zero < z -> forall x y :e R, x <= y -> x * z <= y * z.

Dieudonne_2_2_13c : TMUiRpzhWw824NJCDZZwRz9J5x9UTkBYmud
forall z :e R, zero < z -> forall x y :e R, x * z <= y * z -> x <= y.

Dieudonne_2_2_13d : TMF4NP89Pvf9MrXNtoV7grb1qVW5RnkVbXs
forall z :e R, zero < z -> forall x y :e R, x < y -> x * z < y * z.

Dieudonne_2_2_13e : TMMChUyNEWu2AjrYZuFCnJzkFm18WiNnqmh
forall z :e R, zero < z -> forall x y :e R, x * z < y * z -> x < y.

Dieudonne_2_2_13f : TMNj9pXyNQcyEXVFfjkPhbFkA6731hpowhN
forall x y :e R, zero < x -> x < y -> zero < 1 :/: y /\ 1 :/: y < 1 :/: x.

Dieudonne_2_2_13g : TMSStDrfuaNrQZKoPwBAptZbRSvynvpbPwT
forall x y :e R, zero < 1 :/: y -> 1 :/: y < 1 :/: x -> zero < x /\ x < y.

Dieudonne_2_2_13h : TMbtZQcrYVNPSfWiv6VDX91zMZEgnsLyqAC
forall x y :e R, zero < x -> x < y -> forall n :e omega :\: {0}, zero < x ^ n /\ x ^ n < y ^ n.

Dieudonne_2_2_13i : TMYzbX9RrYYQTNVrEmdjwQrYdDoHJi2iSe3
forall x y :e R, forall n :e omega :\: {0}, zero < x ^ n /\ x ^ n < y ^ n -> zero < x /\ x < y.

RealsStruct_openints_nonempty : TMUAztjkcX2MziWjE85rPfwPtiZfUHegna1
forall ab :e openints, openint (ab 0) (ab 1) <> 0.

RealsStruct_openints_len_pos : TMFjsbgueLyjMWxJuWXVobcwuRTePPQeppZ
forall ab :e openints, zero < len ab.

Dieudonne_2_2_14 : TMaWca6zJgyEzfaasqaR5MJaW4HUQcKMLDj
forall n :e omega, forall J :e openints :^: n, (forall j :e n, forall i :e j, J i :/\: J j = 0) -> forall I :e openints, finsequnion n J c= I -> finseqsum n (fun i :e n => len (J i)) <= len I.

Dieudonne_2_2_15 : TMRZFYxZ42t8umJpqx3uKLpMHPSTnpztm6u
equip omega Q.

Dieudonne_2_2_16 : TMHsUUxAuxsQyVEMaLUZVzMpypsxWoBToJ8
forall ab :e openints, infinite (openint (ab 0) (ab 1) :/\: Q).

Dieudonne_2_2_17a : TMRaUEd1M8sCC17efx2CfZnTGJmYyPU1i14
forall f:set -> set, ~surj omega R f.

Dieudonne_2_2_17b : TMaF2fpR4aAyUNKKMfc8BAvxkHrU6mBoLej
~equip omega R.