PFun

Statistics

Metric	Count
Definitions `PFun`, `Dom`, `asSubtype`, `bind`, `comp`, `core`, `equivSubtype`, `evalOpt`, `fix`, `fixInduction`, `fixInduction'`, `fn`, `graph`, `graph'`, `id`, `image`, `inhabited`, `map`, `monad`, `preimage`, `prodLift`, `prodMap`, `pure`, `ran`, `res`, `restrict`, `toSubtype`, `_»`	28
Theorems `bind_comp`, `Preimage_def`, `asSubtype_eq_of_mem`, `bind_apply`, `bind_defined`, `coe_comp`, `coe_id`, `coe_preimage`, `coe_val`, `comp_apply`, `comp_assoc`, `comp_id`, `compl_dom_subset_core`, `core_def`, `core_eq`, `core_inter`, `core_mono`, `core_res`, `core_restrict`, `dom_coe`, `dom_comp`, `dom_eq`, `dom_iff_graph`, `dom_mk`, `dom_of_mem_fix`, `dom_prodLift`, `dom_prodMap`, `dom_toSubtype`, `dom_toSubtype_apply_iff`, `ext`, `ext'`, `ext_iff`, `fixInduction'_fwd`, `fixInduction'_stop`, `fixInduction_spec`, `fix_fwd`, `fix_fwd_eq`, `fix_stop`, `fn_apply`, `get_prodLift`, `get_prodMap`, `id_apply`, `id_comp`, `image_def`, `image_inter`, `image_mono`, `image_union`, `lawfulMonad`, `lift_graph`, `lift_injective`, `mem_core`, `mem_core_res`, `mem_dom`, `mem_fix_iff`, `mem_image`, `mem_preimage`, `mem_prodLift`, `mem_prodMap`, `mem_res`, `mem_restrict`, `mem_toSubtype_iff`, `preimage_asSubtype`, `preimage_comp`, `preimage_eq`, `preimage_inter`, `preimage_mono`, `preimage_subset_core`, `preimage_subset_dom`, `preimage_union`, `preimage_univ`, `prodLift_apply`, `prodLift_fst_comp_snd_comp`, `prodMap_apply`, `prodMap_comp_comp`, `prodMap_id_id`, `pure_defined`, `res_univ`, `toSubtype_apply`	78
Total	106

PFun

Definitions

Name	Category	Theorems
`Dom` 📖	CompOp	19 math math: `preimage_eq`, `preimage_asSubtype`, `core_eq`, `pure_defined`, `Dioph.dom_dioph`, `mem_dom`, `dom_prodLift`, `preimage_univ`, `dom_prodMap`, `dom_iff_graph`, `preimage_subset_dom`, `Dioph.diophPFun_comp1`, `compl_dom_subset_core`, `open_dom_of_pcontinuous`, `dom_coe`, `dom_toSubtype`, `dom_comp`, `dom_mk`, `dom_eq`
`asSubtype` 📖	CompOp	2 math math: `preimage_asSubtype`, `asSubtype_eq_of_mem`
`bind` 📖	CompOp	1 math math: `bind_apply`
`comp` 📖	CompOp	10 math math: `id_comp`, `preimage_comp`, `prodLift_fst_comp_snd_comp`, `coe_comp`, `prodMap_comp_comp`, `dom_comp`, `comp_apply`, `Part.bind_comp`, `comp_assoc`, `comp_id`
`core` 📖	CompOp	14 math math: `mem_core`, `preimage_eq`, `ptendsto_nhds`, `core_eq`, `core_inter`, `core_restrict`, `Filter.ptendsto_def`, `Filter.mem_pmap`, `compl_dom_subset_core`, `mem_core_res`, `preimage_subset_core`, `core_res`, `core_mono`, `core_def`
`equivSubtype` 📖	CompOp	—
`evalOpt` 📖	CompOp	—
`fix` 📖	CompOp	6 math math: `Partrec.fix`, `fix_fwd_eq`, `Partrec.fix_aux`, `fix_stop`, `Turing.ToPartrec.Code.fix_eval`, `mem_fix_iff`
`fixInduction` 📖	CompOp	1 math math: `fixInduction_spec`
`fixInduction'` 📖	CompOp	2 math math: `fixInduction'_stop`, `fixInduction'_fwd`
`fn` 📖	CompOp	2 math math: `fn_apply`, `Dioph.diophPFun_comp1`
`graph` 📖	CompOp	3 math math: `lift_graph`, `Dioph.diophPFun_vec`, `dom_iff_graph`
`graph'` 📖	CompOp	1 math math: `Filter.ptendsto_iff_rtendsto`
`id` 📖	CompOp	5 math math: `id_comp`, `id_apply`, `coe_id`, `prodMap_id_id`, `comp_id`
`image` 📖	CompOp	6 math math: `image_mono`, `image_def`, `image_inter`, `image_union`, `Finset.coe_pimage`, `mem_image`
`inhabited` 📖	CompOp	—
`map` 📖	CompOp	—
`monad` 📖	CompOp	2 math math: `lawfulMonad`, `bind_defined`
`preimage` 📖	CompOp	16 math math: `preimage_eq`, `preimage_asSubtype`, `core_eq`, `coe_preimage`, `preimage_union`, `preimage_univ`, `preimage_comp`, `preimage_subset_dom`, `preimage_mono`, `ptendsto'_nhds`, `preimage_inter`, `preimage_subset_core`, `dom_comp`, `Preimage_def`, `Filter.ptendsto'_def`, `mem_preimage`
`prodLift` 📖	CompOp	4 math math: `dom_prodLift`, `prodLift_fst_comp_snd_comp`, `prodLift_apply`, `mem_prodLift`
`prodMap` 📖	CompOp	6 math math: `prodMap_apply`, `dom_prodMap`, `prodLift_fst_comp_snd_comp`, `mem_prodMap`, `prodMap_id_id`, `prodMap_comp_comp`
`pure` 📖	CompOp	1 math math: `pure_defined`
`ran` 📖	CompOp	—
`res` 📖	CompOp	8 math math: `Filter.tendsto_iff_ptendsto`, `res_univ`, `mem_res`, `Filter.tendsto_iff_ptendsto_univ`, `continuousWithinAt_iff_ptendsto_res`, `Filter.pmap_res`, `mem_core_res`, `core_res`
`restrict` 📖	CompOp	1 math math: `mem_restrict`
`toSubtype` 📖	CompOp	5 math math: `pointedToPartialFun_map`, `mem_toSubtype_iff`, `toSubtype_apply`, `dom_toSubtype`, `dom_toSubtype_apply_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Preimage_def` 📖	mathematical	—	`preimage` `setOf` `Set` `Set.instMembership` `Part` `Part.instMembership`	—	—
`asSubtype_eq_of_mem` 📖	mathematical	`Part` `Part.instMembership` `Set` `Set.instMembership` `Dom`	`asSubtype`	—	`Part.mem_unique` `Part.get_mem`
`bind_apply` 📖	mathematical	—	`bind` `Part.bind`	—	—
`bind_defined` 📖	mathematical	`Set` `Set.instHasSubset` `Dom`	`PFun` `monad`	—	—
`coe_comp` 📖	mathematical	—	`lift` `comp`	—	`ext` `Part.bind_some`
`coe_id` 📖	mathematical	—	`lift` `id`	—	—
`coe_preimage` 📖	mathematical	—	`preimage` `lift` `Set.preimage`	—	`Set.ext`
`coe_val` 📖	mathematical	—	`lift` `Part.some`	—	—
`comp_apply` 📖	mathematical	—	`comp` `Part.bind`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	`ext` `Part.bind_comp`
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext` `Part.bind_some`
`compl_dom_subset_core` 📖	mathematical	—	`Set` `Set.instHasSubset` `Compl.compl` `Set.instCompl` `Dom` `core`	—	`mem_dom`
`core_def` 📖	mathematical	—	`core` `setOf`	—	—
`core_eq` 📖	mathematical	—	`core` `Set` `Set.instUnion` `preimage` `Compl.compl` `Set.instCompl` `Dom`	—	`preimage_eq` `Set.inter_union_distrib_right` `Set.union_comm` `Set.compl_union_self` `Set.inter_univ` `Set.union_eq_self_of_subset_right` `compl_dom_subset_core`
`core_inter` 📖	mathematical	—	`core` `Set` `Set.instInter`	—	`SetRel.core_inter`
`core_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`core`	—	`SetRel.core_mono`
`core_res` 📖	mathematical	—	`core` `res` `Set` `Set.instUnion` `Compl.compl` `Set.instCompl` `Set.preimage`	—	`Set.ext` `mem_core_res` `instIsEmptyFalse`
`core_restrict` 📖	mathematical	—	`core` `lift` `Set.preimage`	—	`Set.ext`
`dom_coe` 📖	mathematical	—	`Dom` `lift` `Set.univ`	—	—
`dom_comp` 📖	mathematical	—	`Dom` `comp` `preimage`	—	`Set.ext`
`dom_eq` 📖	mathematical	—	`Dom` `setOf` `Part` `Part.instMembership`	—	`Set.ext` `mem_dom`
`dom_iff_graph` 📖	mathematical	—	`Set` `Set.instMembership` `Dom` `graph`	—	`Part.dom_iff_mem`
`dom_mk` 📖	mathematical	—	`Dom` `setOf`	—	—
`dom_of_mem_fix` 📖	mathematical	`Part` `Part.instMembership` `fix`	`Part.Dom`	—	`Part.mem_assert_iff` `Exists.fst`
`dom_prodLift` 📖	mathematical	—	`Dom` `prodLift` `setOf` `Part.Dom`	—	—
`dom_prodMap` 📖	mathematical	—	`Dom` `prodMap` `setOf` `Part.Dom`	—	—
`dom_toSubtype` 📖	mathematical	—	`Dom` `toSubtype` `setOf`	—	—
`dom_toSubtype_apply_iff` 📖	mathematical	—	`Part.Dom` `toSubtype`	—	—
`ext` 📖	—	`Part` `Part.instMembership`	—	—	`Part.ext`
`ext'` 📖	—	`Set` `Set.instMembership` `Dom` `fn`	—	—	`Part.ext'`
`ext_iff` 📖	mathematical	—	`Part` `Part.instMembership`	—	`ext`
`fixInduction'_fwd` 📖	mathematical	`Part` `Part.instMembership` `fix`	`fixInduction'`	—	`dom_of_mem_fix` `fix_fwd` `fixInduction_spec` `Part.get_eq_of_mem`
`fixInduction'_stop` 📖	mathematical	`Part` `Part.instMembership` `fix`	`fixInduction'`	—	`dom_of_mem_fix` `fix_fwd` `fixInduction_spec` `Part.get_eq_of_mem`
`fixInduction_spec` 📖	mathematical	`Part` `Part.instMembership` `fix`	`fixInduction` `fix_fwd`	—	`fix_fwd`
`fix_fwd` 📖	—	`Part` `Part.instMembership` `fix`	—	—	`fix_fwd_eq`
`fix_fwd_eq` 📖	mathematical	`Part` `Part.instMembership`	`fix`	—	`Part.ext` `mem_fix_iff` `Part.mem_unique`
`fix_stop` 📖	mathematical	`Part` `Part.instMembership`	`fix`	—	`mem_fix_iff`
`fn_apply` 📖	mathematical	—	`fn` `Part.get`	—	—
`get_prodLift` 📖	mathematical	`Part.Dom` `prodLift`	`Part.get`	—	—
`get_prodMap` 📖	mathematical	`Part.Dom` `prodMap`	`Part.get`	—	—
`id_apply` 📖	mathematical	—	`id` `Part.some`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`image_def` 📖	mathematical	—	`image` `setOf` `Set` `Set.instMembership` `Part` `Part.instMembership`	—	—
`image_inter` 📖	mathematical	—	`Set` `Set.instHasSubset` `image` `Set.instInter`	—	`SetRel.image_inter_subset`
`image_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`image`	—	`SetRel.image_mono`
`image_union` 📖	mathematical	—	`image` `Set` `Set.instUnion`	—	`SetRel.image_union`
`lawfulMonad` 📖	mathematical	—	`PFun` `monad`	—	`Part.bind_some` `Part.bind_assoc` `Part.bind_some_eq_map`
`lift_graph` 📖	mathematical	—	`Set` `Set.instMembership` `graph` `lift`	—	—
`lift_injective` 📖	mathematical	—	`PFun` `lift`	—	`Part.some_injective`
`mem_core` 📖	mathematical	—	`Set` `Set.instMembership` `core`	—	—
`mem_core_res` 📖	mathematical	—	`Set` `Set.instMembership` `core` `res`	—	—
`mem_dom` 📖	mathematical	—	`Set` `Set.instMembership` `Dom` `Part` `Part.instMembership`	—	—
`mem_fix_iff` 📖	mathematical	—	`Part` `Part.instMembership` `fix`	—	`Part.mem_assert_iff` `Part.mem_assert` `Part.mem_unique`
`mem_image` 📖	mathematical	—	`Set` `Set.instMembership` `image` `Part` `Part.instMembership`	—	—
`mem_preimage` 📖	mathematical	—	`Set` `Set.instMembership` `preimage` `Part` `Part.instMembership`	—	—
`mem_prodLift` 📖	mathematical	—	`Part` `Part.instMembership` `prodLift`	—	—
`mem_prodMap` 📖	mathematical	—	`Part` `Part.instMembership` `prodMap`	—	—
`mem_res` 📖	mathematical	—	`Part` `Part.instMembership` `res` `Set` `Set.instMembership`	—	`Set.subset_univ`
`mem_restrict` 📖	mathematical	`Set` `Set.instHasSubset` `Dom`	`Part` `Part.instMembership` `restrict` `Set.instMembership`	—	—
`mem_toSubtype_iff` 📖	mathematical	—	`Part` `Part.instMembership` `toSubtype`	—	`toSubtype_apply` `Part.mem_mk_iff` `exists_subtype_mk_eq_iff`
`preimage_asSubtype` 📖	mathematical	—	`Set.preimage` `Set.Elem` `Dom` `asSubtype` `Set` `Set.instMembership` `preimage`	—	`Set.ext` `Part.get_mem` `Part.mem_unique`
`preimage_comp` 📖	mathematical	—	`preimage` `comp`	—	—
`preimage_eq` 📖	mathematical	—	`preimage` `Set` `Set.instInter` `core` `Dom`	—	`Set.eq_of_subset_of_subset` `Set.subset_inter` `preimage_subset_core` `preimage_subset_dom` `Part.get_mem`
`preimage_inter` 📖	mathematical	—	`Set` `Set.instHasSubset` `preimage` `Set.instInter`	—	`SetRel.preimage_inter_subset`
`preimage_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`preimage`	—	`SetRel.preimage_mono`
`preimage_subset_core` 📖	mathematical	—	`Set` `Set.instHasSubset` `preimage` `core`	—	`Part.mem_unique`
`preimage_subset_dom` 📖	mathematical	—	`Set` `Set.instHasSubset` `preimage` `Dom`	—	`Part.dom_iff_mem`
`preimage_union` 📖	mathematical	—	`preimage` `Set` `Set.instUnion`	—	`SetRel.preimage_union`
`preimage_univ` 📖	mathematical	—	`preimage` `Set.univ` `Dom`	—	`Set.ext`
`prodLift_apply` 📖	mathematical	—	`prodLift` `Part.Dom` `Part.get`	—	—
`prodLift_fst_comp_snd_comp` 📖	mathematical	—	`prodLift` `comp` `lift` `prodMap`	—	`ext` `Part.bind_some` `Part.get.congr_simp`
`prodMap_apply` 📖	mathematical	—	`prodMap` `Part.Dom` `Part.get`	—	—
`prodMap_comp_comp` 📖	mathematical	—	`prodMap` `comp`	—	`ext`
`prodMap_id_id` 📖	mathematical	—	`prodMap` `id`	—	`ext`
`pure_defined` 📖	mathematical	—	`Set` `Set.instHasSubset` `Dom` `pure`	—	`Set.subset_univ`
`res_univ` 📖	mathematical	—	`res` `Set.univ` `lift`	—	—
`toSubtype_apply` 📖	mathematical	—	`toSubtype`	—	—

PFun.Part

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind_comp` 📖	mathematical	—	`Part.bind` `PFun.comp`	—	`Part.ext`

(root)

Definitions

Name	Category	Theorems
`PFun` 📖	CompOp	7 math math: `PFun.lawfulMonad`, `Nat.Partrec.Code.instCountableSubtypePFunPartrec`, `PFun.lift_injective`, `instIsPreorderPFunNatTuringReducible`, `TuringEquivalent.equivalence`, `PFun.bind_defined`, `recursiveIn_empty_iff_partrec`
`«term_→._»` 📖	CompOp	—

---

← Back to Index