Basic

📁 Source: Mathlib/Data/Prod/Basic.lean

Statistics

Metric	Count
Definitions `decidable`, `delabProdFst`, `delabProdSnd`, `getPPNumericProjProd`, `prod`, `injArrow`	6
Theorems `prodMap`, `prodMap`, `prodMap`, `prodMap`, `prodMap`, `swap_map`, `prodMap`, `refl_left`, `refl_right`, `trans`, `eq_iff_fst_eq_snd_eq`, `exists'`, `forall'`, `fst_comp_mk`, `fst_eq_iff`, `fst_injective`, `fst_surjective`, `id_prod`, `instAntisymmLexOfIsStrictOrder`, `instAsymmLex_mathlib`, `instIrreflLex_mathlib`, `instIsTransLex`, `instReflLex_mathlib`, `instReflLex_mathlib_1`, `lex_iff`, `map_apply'`, `map_bijective`, `map_def`, `map_fst'`, `map_injective`, `map_involutive`, `map_iterate`, `map_leftInverse`, `map_rightInverse`, `map_snd'`, `map_surjective`, `eta`, `mk_inj`, `mk_left_inj`, `mk_left_injective`, `mk_right_inj`, `mk_right_injective`, `snd_comp_mk`, `snd_eq_iff`, `snd_injective`, `snd_surjective`, `swap_bijective`, `swap_eq_iff_eq_swap`, `swap_injective`, `swap_leftInverse`, `swap_rightInverse`, `swap_surjective`, `total_left`, `total_right`, `trichotomous`	55
Total	61

Function.Bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodMap` 📖	—	`Function.Bijective`	—	—	`Function.Injective.prodMap` `Function.Surjective.prodMap`

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodMap` 📖	—	—	—	—	—

Function.Involutive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodMap` 📖	—	`Function.Involutive`	—	—	`Function.LeftInverse.prodMap`

Function.LeftInverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodMap` 📖	—	—	—	—	`comp_eq_id`

Function.RightInverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodMap` 📖	—	—	—	—	`Function.LeftInverse.prodMap`

Function.Semiconj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap_map` 📖	mathematical	—	`Function.Semiconj`	—	`Function.semiconj_iff_comp_eq`

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodMap` 📖	—	—	—	—	—

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_iff_fst_eq_snd_eq` 📖	—	—	—	—	—
`exists'` 📖	—	—	—	—	—
`forall'` 📖	—	—	—	—	—
`fst_comp_mk` 📖	—	—	—	—	—
`fst_eq_iff` 📖	—	—	—	—	—
`fst_injective` 📖	—	—	—	—	—
`fst_surjective` 📖	—	—	—	—	—
`id_prod` 📖	—	—	—	—	—
`instAntisymmLexOfIsStrictOrder` 📖	—	—	—	—	`irrefl` `IsStrictOrder.toIrrefl` `trans` `IsStrictOrder.toIsTrans` `antisymm`
`instAsymmLex_mathlib` 📖	—	—	—	—	—
`instIrreflLex_mathlib` 📖	—	—	—	—	`irrefl`
`instIsTransLex` 📖	mathematical	—	`IsTrans`	—	`Lex.trans`
`instReflLex_mathlib` 📖	—	—	—	—	`Lex.refl_left`
`instReflLex_mathlib_1` 📖	—	—	—	—	`Lex.refl_right`
`lex_iff` 📖	—	—	—	—	—
`map_apply'` 📖	—	—	—	—	—
`map_bijective` 📖	mathematical	—	`Function.Bijective`	—	`Iff.and` `map_injective` `map_surjective` `Nonempty.map`
`map_def` 📖	—	—	—	—	—
`map_fst'` 📖	—	—	—	—	—
`map_injective` 📖	—	—	—	—	`Function.Injective.prodMap`
`map_involutive` 📖	mathematical	—	`Function.Involutive`	—	`map_leftInverse`
`map_iterate` 📖	mathematical	—	`Nat.iterate`	—	—
`map_leftInverse` 📖	—	—	—	—	`Function.LeftInverse.prodMap`
`map_rightInverse` 📖	—	—	—	—	`map_leftInverse`
`map_snd'` 📖	—	—	—	—	—
`map_surjective` 📖	—	—	—	—	`Function.Surjective.prodMap`
`mk_inj` 📖	—	—	—	—	—
`mk_left_inj` 📖	—	—	—	—	`mk_left_injective`
`mk_left_injective` 📖	—	—	—	—	—
`mk_right_inj` 📖	—	—	—	—	`mk_right_injective`
`mk_right_injective` 📖	—	—	—	—	—
`snd_comp_mk` 📖	—	—	—	—	—
`snd_eq_iff` 📖	—	—	—	—	—
`snd_injective` 📖	—	—	—	—	—
`snd_surjective` 📖	—	—	—	—	—
`swap_bijective` 📖	mathematical	—	`Function.Bijective`	—	`swap_injective` `swap_surjective`
`swap_eq_iff_eq_swap` 📖	—	—	—	—	—
`swap_injective` 📖	—	—	—	—	`swap_leftInverse`
`swap_leftInverse` 📖	—	—	—	—	—
`swap_rightInverse` 📖	—	—	—	—	—
`swap_surjective` 📖	—	—	—	—	`Function.LeftInverse.surjective` `swap_leftInverse`
`total_left` 📖	—	—	—	—	—
`total_right` 📖	—	—	—	—	`trichotomous_of` `total_of`
`trichotomous` 📖	—	—	—	—	`trichotomous_of` `Or.imp3`

Prod.Lex

Definitions

Name	Category	Theorems
`decidable` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`refl_left` 📖	—	—	—	—	`refl`
`refl_right` 📖	—	—	—	—	`refl`
`trans` 📖	—	—	—	—	`trans`

Prod.PrettyPrinting

Definitions

Name	Category	Theorems
`delabProdFst` 📖	CompOp	—
`delabProdSnd` 📖	CompOp	—
`getPPNumericProjProd` 📖	CompOp	—

Prod.PrettyPrinting.pp.numericProj

Definitions

Name	Category	Theorems
`prod` 📖	CompOp	—

Prod.mk

Definitions

Name	Category	Theorems
`injArrow` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eta` 📖	—	—	—	—	—

---

← Back to Index