InsertAndContractNat

📁 Source: PhysLean/QFT/PerturbationTheory/WickContraction/InsertAndContractNat.lean

Statistics

Metric	Count
Definitions `insertAndContractNat`, `insertLift`, `insertLiftSome`	3
Theorems `erase_insert`, `insertAndContractNat_bijective`, `insertAndContractNat_erase`, `insertAndContractNat_fstFieldOfContract`, `insertAndContractNat_getDualErase`, `insertAndContractNat_injective`, `insertAndContractNat_none_getDual?_eq_none`, `insertAndContractNat_none_getDual?_isNone`, `insertAndContractNat_none_uncontracted`, `insertAndContractNat_of_isSome`, `insertAndContractNat_sndFieldOfContract`, `insertAndContractNat_some_getDual?_eq`, `insertAndContractNat_some_getDual?_neq_isSome`, `insertAndContractNat_some_getDual?_neq_isSome_get`, `insertAndContractNat_some_getDual?_neq_none`, `insertAndContractNat_some_getDual?_of_neq`, `insertAndContractNat_some_uncontracted`, `insertAndContractNat_succAbove_getDual?_eq_none_iff`, `insertAndContractNat_succAbove_getDual?_get`, `insertAndContractNat_succAbove_getDual?_isSome_iff`, `insertAndContractNat_succAbove_mem_uncontracted_iff`, `insertAndContractNat_surjective_on_nodual`, `insertLiftSome_bijective`, `insertLiftSome_injective`, `insertLiftSome_surjective`, `insertLift_injective`, `insertLift_none_bijective`, `insertLift_none_surjective`, `mem_uncontracted_insertAndContractNat_none_iff`, `mem_uncontracted_insertAndContractNat_some_iff`, `self_mem_uncontracted_of_insertAndContractNat_none`, `self_not_mem_uncontracted_of_insertAndContractNat_some`	32
Total	35

WickContraction

Definitions

Name	Category	Theorems
`insertAndContractNat` 📖	CompOp	36 math math: `insertAndContractNat_getDualErase`, `insertLiftSome_bijective`, `insertAndContract_fstFieldOfContract`, `insertLiftSome_surjective`, `insertAndContractNat_some_getDual?_neq_none`, `insertAndContractNat_some_getDual?_of_neq`, `erase_insert`, `insertAndContractNat_succAbove_mem_uncontracted_iff`, `insertLiftSome_injective`, `insertAndContract_sndFieldOfContract`, `insertAndContractNat_bijective`, `insertLift_injective`, `self_mem_uncontracted_of_insertAndContractNat_none`, `insertAndContract_sndFieldOfContract_some_incl`, `insertAndContractNat_some_uncontracted`, `insertAndContractNat_sndFieldOfContract`, `insertAndContractNat_some_getDual?_eq`, `mem_uncontracted_insertAndContractNat_none_iff`, `insertAndContractNat_fstFieldOfContract`, `insertAndContractNat_injective`, `insertLift_none_surjective`, `insertAndContractNat_succAbove_getDual?_isSome_iff`, `insertAndContractNat_succAbove_getDual?_eq_none_iff`, `insertAndContractNat_erase`, `insertAndContractNat_none_uncontracted`, `insertAndContractNat_of_isSome`, `insertAndContractNat_none_getDual?_eq_none`, `insertAndContract_some_prod_contractions`, `self_not_mem_uncontracted_of_insertAndContractNat_some`, `insertLift_none_bijective`, `insertAndContractNat_none_getDual?_isNone`, `insertAndContract_none_prod_contractions`, `insertAndContract_fstFieldOfContract_some_incl`, `insertAndContractNat_some_getDual?_neq_isSome`, `insertAndContractNat_surjective_on_nodual`, `mem_uncontracted_insertAndContractNat_some_iff`
`insertLift` 📖	CompOp	9 math math: `insertAndContract_fstFieldOfContract`, `insertAndContract_sndFieldOfContract`, `insertLift_injective`, `insertAndContractNat_sndFieldOfContract`, `insertAndContractNat_fstFieldOfContract`, `insertLift_none_surjective`, `insertAndContract_some_prod_contractions`, `insertLift_none_bijective`, `insertAndContract_none_prod_contractions`
`insertLiftSome` 📖	CompOp	3 math math: `insertLiftSome_bijective`, `insertLiftSome_surjective`, `insertLiftSome_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`erase_insert` 📖	mathematical	—	`insertAndContractNat` `erase` `getDualErase`	—	`mem_not_eq_erase_of_isNone` `getDual?_one_eq_none` `getDualErase_isSome_iff_getDual?_isSome` `insertAndContractNat_of_isSome` `PhysLean.Fin.succsAbove_predAboveI` `mem_not_eq_erase_of_isSome`
`insertAndContractNat_bijective` 📖	mathematical	—	`WickContraction` `getDual?` `insertAndContractNat` `uncontracted` `insertAndContractNat_none_getDual?_eq_none`	—	`insertAndContractNat_none_getDual?_eq_none` `insertAndContractNat_injective` `insertAndContractNat_surjective_on_nodual`
`insertAndContractNat_erase` 📖	mathematical	—	`erase` `insertAndContractNat`	—	`eq_filter_mem_self`
`insertAndContractNat_fstFieldOfContract` 📖	mathematical	—	`fstFieldOfContract` `insertAndContractNat` `insertLift`	—	`eq_fstFieldOfContract_of_mem` `fstFieldOfContract_lt_sndFieldOfContract`
`insertAndContractNat_getDualErase` 📖	mathematical	—	`getDualErase` `insertAndContractNat` `uncontracted` `erase` `uncontractedCongr` `WickContraction` `insertAndContractNat_erase`	—	`insertAndContractNat_erase` `uncontractedCongr_none` `insertAndContractNat_none_getDual?_eq_none` `insertAndContractNat_some_getDual?_eq` `PhysLean.Fin.predAboveI_succAbove` `uncontractedCongr_some`
`insertAndContractNat_injective` 📖	mathematical	—	`WickContraction` `insertAndContractNat` `uncontracted`	—	—
`insertAndContractNat_none_getDual?_eq_none` 📖	mathematical	—	`getDual?` `insertAndContractNat` `uncontracted`	—	—
`insertAndContractNat_none_getDual?_isNone` 📖	mathematical	—	`getDual?` `insertAndContractNat` `uncontracted`	—	—
`insertAndContractNat_none_uncontracted` 📖	mathematical	—	`uncontracted` `insertAndContractNat`	—	—
`insertAndContractNat_of_isSome` 📖	mathematical	`uncontracted`	`insertAndContractNat`	—	—
`insertAndContractNat_sndFieldOfContract` 📖	mathematical	—	`sndFieldOfContract` `insertAndContractNat` `insertLift`	—	`eq_sndFieldOfContract_of_mem` `fstFieldOfContract_lt_sndFieldOfContract`
`insertAndContractNat_some_getDual?_eq` 📖	mathematical	—	`getDual?` `insertAndContractNat` `uncontracted`	—	`getDual?_eq_some_iff_mem`
`insertAndContractNat_some_getDual?_neq_isSome` 📖	mathematical	—	`getDual?` `insertAndContractNat` `uncontracted`	—	—
`insertAndContractNat_some_getDual?_neq_isSome_get` 📖	—	`getDual?` `insertAndContractNat` `uncontracted`	—	—	`getDual?_eq_some_iff_mem`
`insertAndContractNat_some_getDual?_neq_none` 📖	mathematical	—	`getDual?` `insertAndContractNat` `uncontracted`	—	—
`insertAndContractNat_some_getDual?_of_neq` 📖	mathematical	—	`getDual?` `insertAndContractNat` `uncontracted`	—	`insertAndContractNat_some_getDual?_neq_isSome_get`
`insertAndContractNat_some_uncontracted` 📖	mathematical	—	`uncontracted` `insertAndContractNat`	—	—
`insertAndContractNat_succAbove_getDual?_eq_none_iff` 📖	mathematical	—	`getDual?` `insertAndContractNat` `uncontracted`	—	`insertAndContractNat_succAbove_mem_uncontracted_iff`
`insertAndContractNat_succAbove_getDual?_get` 📖	—	`getDual?` `insertAndContractNat` `uncontracted`	—	—	`getDual?_eq_some_iff_mem`
`insertAndContractNat_succAbove_getDual?_isSome_iff` 📖	mathematical	—	`getDual?` `insertAndContractNat` `uncontracted`	—	—
`insertAndContractNat_succAbove_mem_uncontracted_iff` 📖	mathematical	—	`uncontracted` `insertAndContractNat`	—	`mem_uncontracted_iff_not_contracted`
`insertAndContractNat_surjective_on_nodual` 📖	mathematical	`getDual?`	`insertAndContractNat` `uncontracted`	—	`mem_uncontracted_iff_not_contracted` `finset_eq_fstFieldOfContract_sndFieldOfContract`
`insertLiftSome_bijective` 📖	mathematical	—	`insertAndContractNat` `uncontracted` `insertLiftSome`	—	`insertLiftSome_injective` `insertLiftSome_surjective`
`insertLiftSome_injective` 📖	mathematical	—	`insertAndContractNat` `uncontracted` `insertLiftSome`	—	`finset_eq_fstFieldOfContract_sndFieldOfContract` `insertLift_injective`
`insertLiftSome_surjective` 📖	mathematical	—	`insertAndContractNat` `uncontracted` `insertLiftSome`	—	—
`insertLift_injective` 📖	mathematical	—	`insertAndContractNat` `insertLift`	—	—
`insertLift_none_bijective` 📖	mathematical	—	`insertAndContractNat` `uncontracted` `insertLift`	—	`insertLift_injective` `insertLift_none_surjective`
`insertLift_none_surjective` 📖	mathematical	—	`insertAndContractNat` `uncontracted` `insertLift`	—	—
`mem_uncontracted_insertAndContractNat_none_iff` 📖	mathematical	—	`uncontracted` `insertAndContractNat`	—	—
`mem_uncontracted_insertAndContractNat_some_iff` 📖	mathematical	—	`uncontracted` `insertAndContractNat`	—	`mem_uncontracted_iff_not_contracted`
`self_mem_uncontracted_of_insertAndContractNat_none` 📖	mathematical	—	`uncontracted` `insertAndContractNat`	—	`mem_uncontracted_iff_not_contracted`
`self_not_mem_uncontracted_of_insertAndContractNat_some` 📖	mathematical	—	`uncontracted` `insertAndContractNat`	—	`mem_uncontracted_iff_not_contracted`

---

← Back to Index