Documentation Verification Report

Part

📁 Source: Mathlib/Order/Part.lean

Statistics

Metric	Count
Definitions `partBind`, `Part`	2
Theorems `partBind`, `partMap`, `partSeq`, `partBind`, `partMap`, `partSeq`, `partBind_coe`	7
Total	9

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`partBind` 📖	mathematical	`Antitone` `Part` `PartialOrder.toPreorder` `Part.instPartialOrder` `Pi.preorder`	`Part.bind`	—	—
`partMap` 📖	mathematical	`Antitone` `Part` `PartialOrder.toPreorder` `Part.instPartialOrder`	`Part.map`	—	`partBind` `antitone_const`
`partSeq` 📖	mathematical	`Antitone` `Part` `PartialOrder.toPreorder` `Part.instPartialOrder`	`Part.instMonad`	—	`Part.instLawfulMonad` `partBind` `of_apply₂` `partMap`

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`partBind` 📖	mathematical	`Monotone` `Part` `PartialOrder.toPreorder` `Part.instPartialOrder` `Pi.preorder`	`Part.bind`	—	—
`partMap` 📖	mathematical	`Monotone` `Part` `PartialOrder.toPreorder` `Part.instPartialOrder`	`Part.map`	—	`partBind` `monotone_const`
`partSeq` 📖	mathematical	`Monotone` `Part` `PartialOrder.toPreorder` `Part.instPartialOrder`	`Part.instMonad`	—	`Part.instLawfulMonad` `partBind` `of_apply₂` `partMap`

OrderHom

Definitions

Name	Category	Theorems
`partBind` 📖	CompOp	2 math math: `OmegaCompletePartialOrder.ContinuousHom.ωSup_bind`, `partBind_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`partBind_coe` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Part` `PartialOrder.toPreorder` `Part.instPartialOrder` `instFunLike` `partBind` `Part.bind` `Pi.preorder`	—	—

(root)

Definitions

Name	Category	Theorems
`Part` 📖	CompData	125 math math: `Part.mem_bind_iff`, `Partrec.merge'`, `Part.inter_def`, `Part.one_mem_one`, `Part.append_def`, `Part.Fix.exists_fix_le_approx`, `Turing.ToPartrec.Code.comp_eval`, `Part.mem_mk_iff`, `Part.neg_some`, `pointedToPartialFun_map`, `Part.add_def`, `Part.one_def`, `Part.some_injective`, `Part.mem_ofOption`, `Turing.ToPartrec.Code.nil_eval`, `Part.toUnitMono_coe`, `Nat.rfind_dom`, `Turing.tr_eval'`, `Nat.Partrec.prec'`, `Turing.ToPartrec.Code.pred_eval`, `Part.Fix.approx_mem_approxChain`, `Part.eq_some_iff`, `Nat.rfind_min'`, `Part.Fix.approx_le_fix`, `Turing.ToPartrec.Code.head_eval`, `Turing.ToPartrec.stepNormal_eval`, `Part.mem_some_iff`, `Part.some_add_some`, `Part.bind_le`, `Part.get_eq_get_of_eq`, `Part.some_inter_some`, `Part.some_union_some`, `Turing.ToPartrec.Cont.then_eval`, `Turing.ToPartrec.Code.zero'_eval`, `Turing.ToPartrec.Code.tail_eval`, `PFun.mem_dom`, `Part.Mem.right_unique`, `PFun.image_def`, `Turing.ToPartrec.Code.id_eval`, `Part.coe_toFinset`, `OmegaCompletePartialOrder.ContinuousHom.bind_apply`, `OmegaCompletePartialOrder.ContinuousHom.seq_apply`, `Part.ext_iff`, `Nat.mem_rfind`, `Part.mem_toOption`, `Part.div_def`, `PFun.mem_res`, `Turing.mem_eval`, `PFun.mem_restrict`, `Part.get_mem`, `Finset.mem_pimage`, `Part.mem_restrict`, `Part.map_eq_map`, `Part.eq_get_iff_mem`, `Nat.Partrec.rfind'`, `Nat.Partrec.Code.eval_prec_succ`, `Partrec.merge`, `Part.mem_coe`, `Partrec₂.unpaired'`, `Part.subsingleton`, `Part.some_sdiff_some`, `Part.dom_iff_mem`, `Part.mem_ωSup`, `Vector.mOfFn_part_some`, `Part.mem_some`, `Part.inv_def`, `Part.eq_none_iff`, `Nat.rfindOpt_mono`, `Turing.ToPartrec.Code.cons_eval`, `Turing.ToPartrec.stepRet_eval`, `Part.inv_some`, `Turing.ToPartrec.cont_eval_fix`, `Part.some_sub_some`, `Part.sub_def`, `Part.fix_eq_ωSup`, `PFun.mem_toSubtype_iff`, `Part.instLawfulMonad`, `Part.ret_eq_some`, `Part.Mem.left_unique`, `Part.get_eq_iff_mem`, `Partrec.fix_aux`, `Turing.ToPartrec.Code.exists_code`, `Part.toOption_eq_some_iff`, `Part.mod_def`, `OmegaCompletePartialOrder.ContinuousHom.ωSup_bind`, `Turing.ToPartrec.Code.succ_eval`, `Nat.rfind_dom'`, `Turing.PartrecToTM2.tr_eval`, `Turing.ToPartrec.Code.Ok.zero`, `PFun.mem_prodMap`, `Part.zero_def`, `Nat.Partrec.merge'`, `Part.some_mul_some`, `Part.some_append_some`, `Part.some_mod_some`, `Part.some_div_some`, `Part.sdiff_def`, `PFun.mem_image`, `Part.union_def`, `Part.Fix.approx_mono'`, `Part.mul_def`, `Part.zero_mem_zero`, `Part.notMem_none`, `Partrec₂.unpaired`, `Turing.ToPartrec.Code.zero_eval`, `Turing.ToPartrec.Code.case_eval`, `PFun.mem_fix_iff`, `Part.Fix.mem_iff`, `Part.neg_def`, `Part.mem_map_iff`, `Part.pure_eq_some`, `Nat.Partrec.Code.evaln_sound`, `Nat.Partrec.Code.evaln_complete`, `Part.bind_eq_bind`, `PFun.mem_prodLift`, `Part.mem_toFinset`, `Part.mem_eq`, `PFun.dom_eq`, `PFun.ext_iff`, `Part.mem_assert_iff`, `OmegaCompletePartialOrder.ContinuousHom.map_apply`, `OrderHom.partBind_coe`, `Part.Fix.approx_mono`, `PFun.Preimage_def`, `PFun.mem_preimage`

---

← Back to Index