≝ λA.λeq,ap.∀x,y:A. (\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(ap x y) → eq x y) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6
(eq x y → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(ap x y)).
≝ λA.λeq,ap.∀x,y:A. (\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(ap x y) → eq x y) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6
(eq x y → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(ap x y)).
≝ λA.λR.∀x,y:A. R x y → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(R y x).
(********** functions **********)
≝ λA.λR.∀x,y:A. R x y → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(R y x).
(********** functions **********)
λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
interpretation "function composition" 'compose f g = (compose ? ? ? f g).
λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
interpretation "function composition" 'compose f g = (compose ? ? ? f g).
≝ λA,B.λf.∀x,y:A.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f y → x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y.
≝ λA,B.λf.∀x,y:A.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f y → x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y.
≝λA,B.λf.∀z:B.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6x:A\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x.
≝λA,B.λf.∀z:B.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6x:A\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x.
≝ λA.λf.∀x,y,z.f (f x y) z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x (f y z).
(* functions and relations *)
≝ λA.λf.∀x,y,z.f (f x y) z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x (f y z).
(* functions and relations *)
∀f:A→A.Prop ≝
λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
(* functions and functions *)
∀f:A→A.Prop ≝
λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
(* functions and functions *)
≝ λA.λf,g.∀x,y,z:A. f x (g y z) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g (f x y) (f x z).
≝ λA.λf,g.∀x,y,z:A. f x (g y z) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g (f x y) (f x z).
≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g (f x y) (f x z).
≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g (f x y) (f x z).
-\ 5img class="anchor" src="icons/tick.png" id="injective_compose"\ 6lemma injective_compose : ∀A,B,C,f,g.
+lemma injective_compose : ∀A,B,C,f,g.
\ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 A B f → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 B C g → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 A C (λx.g (f x)).
/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/; qed.
(* extensional equality *)
\ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 A B f → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 B C g → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 A C (λx.g (f x)).
/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/; qed.
(* extensional equality *)
λA,B.λf,g.∀a.f a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g a.
notation " x \eqP y " non associative with precedence 45
λA,B.λf,g.∀a.f a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g a.
notation " x \eqP y " non associative with precedence 45