一応できた。sectionは要らないみたい。
/-! 写像と関係 -/
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
/- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> -/
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
(p : IsInjective f)
(q : IsInjective g)
-- 結論は最初かかないでも、後で足せる。
:=
have p' : ∀(x x' : X),( f x = f x' → x = x' ) := p
have q' : ∀(y y' : Y),( g y = g y' → y = y' ) := q
let con := fun (x x' : X) =>
let r : ∀(x x' : X),( g (f x) = g (f x') → f x = f x' ) :=
fun x x'=> q' (y := f x) (y' := f x')
Cut (r x x') (p' x x')
show ∀(x x' : X),( g (f x) = g (f x') → x = x' ) from con
#check lemma -- {X Y Z : Type} (f : X → Y) (g : Y → Z) (p : IsInjective f) (q : IsInjective g) (x x' : X)
-- (a✝ : g (f x) = g (f x')) : x = x'
#check lemma f g -- IsInjective f → IsInjective g → ∀ (x x' : X), g (f x) = g (f x') → x = x'
def main : target f g :=
fun (p : IsInjective f) (q : IsInjective g) =>
lemma f g p q
#check main
#print main
#print main.proof_1
end -- section
end inj_inj_comp_inj
/- <<<<<<<<<<<<<<<<<<<<<<<<<<<<<< -/
#check inj_inj_comp_inj.main
#print inj_inj_comp_inj.target
end My
#check My.inj_inj_comp_inj.main
#print My.inj_inj_comp_inj.target
