返回 NPA
声明
local_unique_apply
Mathlib.Topology.Metric.Basic
包
2
模块
63
定理
750
声明
1016
非可信 sidecar
源文本和展示 overlay 属于展示元数据。可信证据是签名证书和 checker 结果。
陈述
forall (X : Sort u), forall (Y : Sort v), forall (domain : forall (x : X), Prop), forall (predicate : forall (x : X), forall (y : Y), Prop), forall (candidate : forall (x : X), Y), forall (uniq : @LocalUnique.{u,v} X Y domain predicate candidate), forall (other : forall (x : X), Y), forall (other_sol : forall (x : X), forall (hx : domain x), predicate x (other x)), forall (candidate_sol : forall (x : X), forall (hx : domain x), predicate x (candidate x)), @LocalEq.{u,v} X Y domain other candidate证明项
fun X => fun Y => fun domain => fun predicate => fun candidate => fun uniq => fun other => fun other_sol => fun candidate_sol => uniq other other_sol candidate_sol