KerSetoid

Mathlib.Algebra.Group.Kernel.Quotient

包

模块

定理

750

声明

1016

非可信 sidecar

源文本和展示 overlay 属于展示元数据。可信证据是签名证书和 checker 结果。

陈述

forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), @Setoid.{u} G

证明项

fun G => fun H => fun f => @Setoid.mk.{u} G (@KerRel.{succ u,succ v} G H f) (fun (P : Prop) => fun (mk_equiv : forall (refl_arg : forall (x : G), @KerRel.{succ u,succ v} G H f x x), forall (symm_arg : forall (x : G), forall (y : G), forall (p : @KerRel.{succ u,succ v} G H f x y), @KerRel.{succ u,succ v} G H f y x), forall (trans_arg : forall (x : G), forall (y : G), forall (z : G), forall (p : @KerRel.{succ u,succ v} G H f x y), forall (q : @KerRel.{succ u,succ v} G H f y z), @KerRel.{succ u,succ v} G H f x z), P) => mk_equiv (@ker_rel_refl.{succ u,succ v} G H f) (@ker_rel_symm.{succ u,succ v} G H f) (@ker_rel_trans.{succ u,succ v} G H f))