Join

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

Statistics

Metric	Count
Definitions `join`, `joinLift`, `joinLiftLeft`, `joinLiftRight`	4
Theorems `empty_join`, `exists_contraction_pair_of_card_ge_zero`, `exists_join_singleton_of_card_ge_zero`, `exists_mem_left_uncontracted_of_mem_join_uncontracted`, `exists_mem_right_uncontracted_of_mem_join_uncontracted`, `joinLiftLeft_or_joinLiftRight_of_mem_join`, `joinLiftRight_injective`, `joinLift_bijective`, `joinLift_injective`, `joinLift_surjective`, `join_assoc`, `join_card`, `join_congr`, `join_empty`, `join_fstFieldOfContract_joinLiftLeft`, `join_fstFieldOfContract_joinLiftRight`, `join_getDual?_apply_uncontractedListEmb`, `join_getDual?_apply_uncontractedListEmb_eq_none_iff`, `join_getDual?_apply_uncontractedListEmb_isSome_iff`, `join_getDual?_apply_uncontractedListEmb_some`, `join_not_gradingCompliant_of_left_not_gradingCompliant`, `join_singleton_getDual?_left`, `join_singleton_getDual?_right`, `join_sndFieldOfContract_joinLift`, `join_sndFieldOfContract_joinLiftRight`, `join_staticContract`, `join_sub_quot`, `join_timeContract`, `join_uncontractedList`, `join_uncontractedListEmb`, `join_uncontractedListGet`, `join_uncontractedList_get`, `jointLiftLeft_disjoint_joinLiftRight`, `jointLiftLeft_injective`, `jointLiftLeft_neq_joinLiftRight`, `mem_join_right_iff`, `mem_join_uncontracted_of_mem_right_uncontracted`, `prod_join`, `subContraction_card_plus_quotContraction_card_eq`	39
Total	43

WickContraction

Definitions

Name	Category	Theorems
`join` 📖	CompOp	47 math math: `join_getDual?_apply_uncontractedListEmb_eq_none_iff`, `join_singleton_signFinset_eq_filter`, `signFinset_right_map_uncontractedListEmd_eq_filter`, `EqTimeOnly.exists_join_singleton_of_card_ge_zero`, `sign_right_eq_prod_mul_prod`, `join_fstFieldOfContract_joinLiftRight`, `join_singleton_sign_right`, `join_sign_timeContract`, `join_card`, `jointLiftLeft_injective`, `joinLift_injective`, `mem_join_right_iff`, `joinLift_surjective`, `join_empty`, `join_assoc`, `join_fstFieldOfContract_joinLiftLeft`, `EqTimeOnly.exists_join_singleton_of_not_eqTimeOnly`, `join_singleton_sign_left`, `join_timeContract`, `join_staticContract`, `join_eqTimeContractSet`, `join_uncontractedListEmb`, `join_sign`, `join_sub_quot`, `join_getDual?_apply_uncontractedListEmb_isSome_iff`, `join_getDual?_apply_uncontractedListEmb`, `join_not_gradingCompliant_of_left_not_gradingCompliant`, `join_singleton_getDual?_left`, `join_sndFieldOfContract_joinLift`, `sum_haveEqTime`, `exists_join_singleton_of_card_ge_zero`, `join_singleton_getDual?_right`, `jointLiftLeft_disjoint_joinLiftRight`, `join_sign_induction`, `join_uncontractedList_get`, `join_singleton_left_signFinset_eq_filter`, `join_congr`, `prod_join`, `joinLift_bijective`, `join_sndFieldOfContract_joinLiftRight`, `join_uncontractedList`, `join_uncontractedListGet`, `mem_join_uncontracted_of_mem_right_uncontracted`, `joinLiftRight_injective`, `empty_join`, `join_sign_singleton`, `join_haveEqTime_of_eqTimeOnly_nonEmpty`
`joinLift` 📖	CompOp	3 math math: `joinLift_injective`, `joinLift_surjective`, `joinLift_bijective`
`joinLiftLeft` 📖	CompOp	6 math math: `joinLiftLeft_or_joinLiftRight_of_mem_join`, `jointLiftLeft_injective`, `join_fstFieldOfContract_joinLiftLeft`, `join_sndFieldOfContract_joinLift`, `jointLiftLeft_disjoint_joinLiftRight`, `prod_join`
`joinLiftRight` 📖	CompOp	6 math math: `joinLiftLeft_or_joinLiftRight_of_mem_join`, `join_fstFieldOfContract_joinLiftRight`, `jointLiftLeft_disjoint_joinLiftRight`, `prod_join`, `join_sndFieldOfContract_joinLiftRight`, `joinLiftRight_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`empty_join` 📖	mathematical	—	`join` `empty` `FieldSpecification.FieldOp` `WickContraction` `uncontractedListGet` `congr` `uncontractedListGet_empty`	—	`uncontractedListGet_empty` `uncontractedListEmd_empty` `empty.eq_1` `mem_congr_iff`
`exists_contraction_pair_of_card_ge_zero` 📖	—	`FieldSpecification.FieldOp`	—	—	—
`exists_join_singleton_of_card_ge_zero` 📖	mathematical	`FieldSpecification.FieldOp` `GradingCompliant`	`join` `singleton` `FieldSpecification.fieldOpStatistic` `uncontractedListGet`	—	`exists_contraction_pair_of_card_ge_zero` `fstFieldOfContract_lt_sndFieldOfContract` `subContraction_singleton_eq_singleton` `join_congr` `congr_trans_apply` `join_sub_quot` `gradingCompliant_congr` `quotContraction_gradingCompliant` `card_congr` `subContraction_card_plus_quotContraction_card_eq`
`exists_mem_left_uncontracted_of_mem_join_uncontracted` 📖	—	`FieldSpecification.FieldOp` `uncontracted` `join`	—	—	`mem_uncontracted_iff_not_contracted`
`exists_mem_right_uncontracted_of_mem_join_uncontracted` 📖	mathematical	`FieldSpecification.FieldOp` `uncontracted` `join`	`uncontractedListGet` `uncontractedListEmd`	—	`exists_mem_left_uncontracted_of_mem_join_uncontracted` `uncontractedListEmd_surjective_mem_uncontracted` `mem_uncontracted_iff_not_contracted`
`joinLiftLeft_or_joinLiftRight_of_mem_join` 📖	mathematical	`FieldSpecification.FieldOp` `join`	`joinLiftLeft` `joinLiftRight`	—	—
`joinLiftRight_injective` 📖	mathematical	—	`FieldSpecification.FieldOp` `uncontractedListGet` `join` `joinLiftRight`	—	—
`joinLift_bijective` 📖	mathematical	—	`FieldSpecification.FieldOp` `uncontractedListGet` `join` `joinLift`	—	`joinLift_injective` `joinLift_surjective`
`joinLift_injective` 📖	mathematical	—	`FieldSpecification.FieldOp` `uncontractedListGet` `join` `joinLift`	—	`jointLiftLeft_injective` `joinLiftRight_injective` `jointLiftLeft_neq_joinLiftRight`
`joinLift_surjective` 📖	mathematical	—	`FieldSpecification.FieldOp` `uncontractedListGet` `join` `joinLift`	—	—
`join_assoc` 📖	mathematical	—	`join` `uncontractedListGet` `WickContraction` `FieldSpecification.FieldOp` `congr` `join_uncontractedListGet`	—	`join_uncontractedListGet` `join_uncontractedListEmb`
`join_card` 📖	mathematical	—	`FieldSpecification.FieldOp` `join` `uncontractedListGet`	—	`uncontractedListEmd_finset_disjoint_left`
`join_congr` 📖	mathematical	—	`join` `WickContraction` `FieldSpecification.FieldOp` `uncontractedListGet` `congr`	—	—
`join_empty` 📖	mathematical	—	`join` `empty` `FieldSpecification.FieldOp` `uncontractedListGet`	—	—
`join_fstFieldOfContract_joinLiftLeft` 📖	mathematical	—	`fstFieldOfContract` `FieldSpecification.FieldOp` `join` `joinLiftLeft`	—	`eq_fstFieldOfContract_of_mem` `fstFieldOfContract_lt_sndFieldOfContract`
`join_fstFieldOfContract_joinLiftRight` 📖	mathematical	—	`fstFieldOfContract` `FieldSpecification.FieldOp` `join` `joinLiftRight` `uncontractedListGet` `uncontractedListEmd`	—	`eq_fstFieldOfContract_of_mem` `uncontractedListEmd_strictMono` `fstFieldOfContract_lt_sndFieldOfContract`
`join_getDual?_apply_uncontractedListEmb` 📖	mathematical	—	`getDual?` `FieldSpecification.FieldOp` `join` `uncontractedListGet` `uncontractedListEmd`	—	`join_getDual?_apply_uncontractedListEmb_isSome_iff` `join_getDual?_apply_uncontractedListEmb_some`
`join_getDual?_apply_uncontractedListEmb_eq_none_iff` 📖	mathematical	—	`getDual?` `FieldSpecification.FieldOp` `join` `uncontractedListGet` `uncontractedListEmd`	—	`getDual?_eq_none_iff_mem_uncontracted` `exists_mem_right_uncontracted_of_mem_join_uncontracted` `mem_join_uncontracted_of_mem_right_uncontracted`
`join_getDual?_apply_uncontractedListEmb_isSome_iff` 📖	mathematical	—	`FieldSpecification.FieldOp` `getDual?` `join` `uncontractedListGet` `uncontractedListEmd`	—	—
`join_getDual?_apply_uncontractedListEmb_some` 📖	—	`FieldSpecification.FieldOp` `getDual?` `join` `uncontractedListGet` `uncontractedListEmd`	—	—	`getDual?_eq_some_iff_mem`
`join_not_gradingCompliant_of_left_not_gradingCompliant` 📖	mathematical	`GradingCompliant`	`join`	—	`join_fstFieldOfContract_joinLiftLeft` `join_sndFieldOfContract_joinLift`
`join_singleton_getDual?_left` 📖	mathematical	`FieldSpecification.FieldOp`	`getDual?` `join` `singleton`	—	`getDual?_eq_some_iff_mem`
`join_singleton_getDual?_right` 📖	mathematical	`FieldSpecification.FieldOp`	`getDual?` `join` `singleton`	—	`getDual?_eq_some_iff_mem`
`join_sndFieldOfContract_joinLift` 📖	mathematical	—	`sndFieldOfContract` `FieldSpecification.FieldOp` `join` `joinLiftLeft`	—	`eq_sndFieldOfContract_of_mem` `fstFieldOfContract_lt_sndFieldOfContract`
`join_sndFieldOfContract_joinLiftRight` 📖	mathematical	—	`sndFieldOfContract` `FieldSpecification.FieldOp` `join` `joinLiftRight` `uncontractedListGet` `uncontractedListEmd`	—	`eq_sndFieldOfContract_of_mem` `uncontractedListEmd_strictMono` `fstFieldOfContract_lt_sndFieldOfContract`
`join_staticContract` 📖	mathematical	—	`staticContract` `join` `FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `uncontractedListGet`	—	`prod_join` `join_fstFieldOfContract_joinLiftRight` `getElem_uncontractedListEmd` `join_sndFieldOfContract_joinLiftRight`
`join_sub_quot` 📖	mathematical	`FieldSpecification.FieldOp`	`join` `subContraction` `quotContraction`	—	`mem_of_mem_subContraction` `mem_of_mem_quotContraction` `mem_subContraction_or_quotContraction`
`join_timeContract` 📖	mathematical	—	`timeContract` `join` `FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `uncontractedListGet`	—	`prod_join` `join_fstFieldOfContract_joinLiftRight` `getElem_uncontractedListEmd` `join_sndFieldOfContract_joinLiftRight`
`join_uncontractedList` 📖	mathematical	—	`uncontractedList` `FieldSpecification.FieldOp` `join` `uncontractedListGet` `uncontractedListEmd`	—	`uncontractedList_eq_sort` `fin_finset_sort_map_monotone` `uncontractedListEmd_strictMono` `exists_mem_right_uncontracted_of_mem_join_uncontracted` `mem_join_uncontracted_of_mem_right_uncontracted`
`join_uncontractedListEmb` 📖	mathematical	—	`uncontractedListEmd` `join` `FieldSpecification.FieldOp` `uncontractedListGet` `join_uncontractedListGet`	—	`join_uncontractedListGet` `uncontractedListEmd_toFun_eq_get` `join_uncontractedList` `join_uncontractedList_get`
`join_uncontractedListGet` 📖	mathematical	—	`uncontractedListGet` `join`	—	`join_uncontractedList`
`join_uncontractedList_get` 📖	mathematical	—	`FieldSpecification.FieldOp` `uncontractedList` `join` `uncontractedListGet` `uncontractedListEmd` `join_uncontractedList`	—	`join_uncontractedList`
`jointLiftLeft_disjoint_joinLiftRight` 📖	mathematical	—	`FieldSpecification.FieldOp` `join` `joinLiftLeft` `joinLiftRight`	—	`uncontractedListEmd_finset_disjoint_left`
`jointLiftLeft_injective` 📖	mathematical	—	`FieldSpecification.FieldOp` `join` `joinLiftLeft`	—	—
`jointLiftLeft_neq_joinLiftRight` 📖	—	—	—	—	`jointLiftLeft_disjoint_joinLiftRight`
`mem_join_right_iff` 📖	mathematical	—	`FieldSpecification.FieldOp` `uncontractedListGet` `join` `uncontractedListEmd`	—	`uncontractedListEmd_finset_not_mem`
`mem_join_uncontracted_of_mem_right_uncontracted` 📖	mathematical	`FieldSpecification.FieldOp` `uncontractedListGet` `uncontracted`	`join` `uncontractedListEmd`	—	`mem_uncontracted_iff_not_contracted` `uncontractedListEmd_mem_uncontracted`
`prod_join` 📖	mathematical	—	`FieldSpecification.FieldOp` `join` `joinLiftLeft` `uncontractedListGet` `joinLiftRight`	—	`joinLift_bijective`
`subContraction_card_plus_quotContraction_card_eq` 📖	mathematical	`FieldSpecification.FieldOp`	`subContraction` `uncontractedListGet` `quotContraction`	—	`join_card` `join_sub_quot`

---

← Back to Index