/-! 写像と関係 -/
namespace My
/- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> -/
section Logic
def MP {A B: Prop}
(p:A → B) (a: A)
: B
:= p a
def Inst {X: Type} {P: X → Prop}
(w: ∀(x: X), P x) (a : X)
: P a
:= w a
def Cut {A B C : Prop}
(p: A → B) (q: B → C)
: A → C
:= q ∘ p
end Logic
/- <<<<<<<<<<<<<<<<<<<<<<<<<<<<<< -/
#check MP
#check Inst
#check Cut
def IsInjective {X Y: Type} (f: X → Y) : Prop :=
∀(x y : X),( f x = f y → x = y )
#print IsInjective
theorem eq_triv (X : Type) : ∀(x :X),( x = x)
:=
fun (x :X )=>
Eq.refl x
theorem logical_triv (P : Prop) : P → P
:= fun (w: P)=> w
#print logical_triv
theorem id_is_injective' (X : Type)
: ∀(x y : X),( x = y → x = y )
:=
fun (x y : X) =>
fun (w: x = y) => (w : x = y)
#print id_is_injective'
/-
assume some x y :x
assume w: x = Y
we_conclude x = y from w
--/
theorem id_is_injective (X : Type)
: IsInjective (λ(x: X)=> x)
:= id_is_injective' X
#print id_is_injective
theorem id_is_injective_? (X : Type)
(id_is_injective2_? :(X : Type) → ∀(x y : X),( x = y → x = y ) )
: IsInjective (λ(x: X)=> x)
:= id_is_injective2_? X
theorem id_is_injective2_! (X : Type) : ∀(x y : X),( x = y → x = y )
:= fun (x y : X) (w: x = y) => w
theorem id_is_injective_! (X : Type)
: IsInjective (λ(x: X)=> x)
:= id_is_injective_? X (fun X:Type => id_is_injective2_! X)
/- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> -/
namespace inj_inj_comp_inj
section
/-!
## 単射と単射の結合は単射である
-/
variable -- 前提／コンテキスト
{X Y Z : Type}
(f:X → Y) (g: Y → Z)
def target': Prop :=
(IsInjective f) ∧ (IsInjective g) → (IsInjective (g∘f))
#check target' -- {X Y Z : Type} (f : X → Y) (g : Y → Z) : Prop
def target: Prop :=
(IsInjective f) → (IsInjective g) → (IsInjective (g∘f))
#check target -- {X Y Z : Type} (f : X → Y) (g : Y → Z) : Prop
def lemma_1
(q : IsInjective g)
-- : (IsInjective (g∘f))
:=
have _q: ∀(y y' : Y),( g y = g y' → y = y' ) := q
let r : ∀(x y : X),( g (f x) = g (f y) → f x = f y ) :=
fun (x y: X)=> q (x := f x) (y := f y)
show ∀(x y : X),( g (f x) = g (f y) → f x = f y ) from r
def lemma_2
(p : IsInjective f)
(q : IsInjective g)
-- :
:=
have _1 : ∀(x y : X),( g (f x) = g (f y) → f x = f y ) :=
lemma_1 q
def main : target f g := sorry
#check target f g
#check inst_conc
end -- section
end inj_inj_comp_inj
/- <<<<<<<<<<<<<<<<<<<<<<<<<<<<<< -/
theorem inj_inj_comp_inj {X Y Z : Type}
(f:X → Y) (g: Y → Z)
: (IsInjective f) ∧ (IsInjective g) → (IsInjective g∘f)
:=
end My
