Basic

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

Statistics

Metric	Count
Definitions `in₀`, `in₁`, `in₂`	3
Theorems `sumMap`, `sumElim`, `sumMap`, `sumMap`, `inl_injective`, `inr_injective`, `exists_of_isLeft_left`, `exists_of_isLeft_right`, `exists_of_isRight_left`, `exists_of_isRight_right`, `isLeft_congr`, `isLeft_left`, `isLeft_right`, `isRight_congr`, `isRight_left`, `isRight_right`, `elim_injective`, `elim_swap`, `elim_update_left`, `elim_update_right`, `eq_left_iff_getLeft_eq`, `eq_right_iff_getRight_eq`, `exists_sum`, `getLeft_eq_getLeft?`, `getRight_eq_getRight?`, `inl_injective`, `inr_injective`, `isSome_getLeft?_iff_isLeft`, `isSome_getRight?_iff_isRight`, `liftRel_iff`, `map_bijective`, `map_injective`, `map_surjective`, `rec_update_left`, `rec_update_right`, `sum_rec_congr`, `swap_leftInverse`, `swap_rightInverse`, `update_elim_inl`, `update_elim_inr`, `update_inl_apply_inl`, `update_inl_apply_inl'`, `update_inl_apply_inr`, `update_inl_comp_inl`, `update_inl_comp_inr`, `update_inr_apply_inl`, `update_inr_apply_inr`, `update_inr_apply_inr'`, `update_inr_comp_inl`, `update_inr_comp_inr`, `not_isLeft_and_isRight`	51
Total	54

Function.Bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumMap` 📖	—	`Function.Bijective`	—	—	`Function.Injective.sumMap` `injective` `Function.Surjective.sumMap` `surjective`

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumElim` 📖	—	—	—	—	—
`sumMap` 📖	—	—	—	—	—

Function.Surjective

Theorems

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

PSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inl_injective` 📖	—	—	—	—	—
`inr_injective` 📖	—	—	—	—	—

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elim_injective` 📖	—	—	—	—	`inl_injective` `inr_injective` `Function.Injective.sumElim`
`elim_swap` 📖	—	—	—	—	—
`elim_update_left` 📖	mathematical	—	`Function.update`	—	`rec_update_left`
`elim_update_right` 📖	mathematical	—	`Function.update`	—	`rec_update_right`
`eq_left_iff_getLeft_eq` 📖	—	—	—	—	—
`eq_right_iff_getRight_eq` 📖	—	—	—	—	—
`exists_sum` 📖	—	—	—	—	`not_forall_not`
`getLeft_eq_getLeft?` 📖	—	—	—	—	—
`getRight_eq_getRight?` 📖	—	—	—	—	—
`inl_injective` 📖	—	—	—	—	—
`inr_injective` 📖	—	—	—	—	—
`isSome_getLeft?_iff_isLeft` 📖	—	—	—	—	—
`isSome_getRight?_iff_isRight` 📖	—	—	—	—	—
`liftRel_iff` 📖	—	—	—	—	—
`map_bijective` 📖	mathematical	—	`Function.Bijective`	—	`Iff.and` `map_injective` `map_surjective`
`map_injective` 📖	—	—	—	—	`Function.Injective.of_comp` `inl_injective` `inr_injective` `Function.Injective.sumMap`
`map_surjective` 📖	—	—	—	—	`inl_injective` `inr_injective` `Function.Surjective.sumMap`
`rec_update_left` 📖	mathematical	—	`Function.update`	—	`Function.rec_update` `inl_injective`
`rec_update_right` 📖	mathematical	—	`Function.update`	—	`Function.rec_update` `inr_injective`
`sum_rec_congr` 📖	—	—	—	—	—
`swap_leftInverse` 📖	—	—	—	—	—
`swap_rightInverse` 📖	—	—	—	—	—
`update_elim_inl` 📖	mathematical	—	`Function.update`	—	`Function.update_eq_iff` `Function.update_self` `Function.update_of_ne`
`update_elim_inr` 📖	mathematical	—	`Function.update`	—	`Function.update_eq_iff` `Function.update_self` `Function.update_of_ne`
`update_inl_apply_inl` 📖	mathematical	—	`Function.update`	—	—
`update_inl_apply_inl'` 📖	mathematical	—	`Function.update`	—	`Function.update_apply_of_injective` `inl_injective`
`update_inl_apply_inr` 📖	mathematical	—	`Function.update`	—	`Function.update_of_ne`
`update_inl_comp_inl` 📖	mathematical	—	`Function.update`	—	`Function.update_comp_eq_of_injective` `inl_injective`
`update_inl_comp_inr` 📖	mathematical	—	`Function.update`	—	`Function.update_comp_eq_of_forall_ne`
`update_inr_apply_inl` 📖	mathematical	—	`Function.update`	—	`Function.update_of_ne`
`update_inr_apply_inr` 📖	mathematical	—	`Function.update`	—	`update_inr_comp_inr`
`update_inr_apply_inr'` 📖	mathematical	—	`Function.update`	—	`Function.update_apply_of_injective` `inr_injective`
`update_inr_comp_inl` 📖	mathematical	—	`Function.update`	—	`Function.update_comp_eq_of_forall_ne`
`update_inr_comp_inr` 📖	mathematical	—	`Function.update`	—	`Function.update_comp_eq_of_injective` `inr_injective`

Sum.LiftRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_of_isLeft_left` 📖	—	—	—	—	—
`exists_of_isLeft_right` 📖	—	—	—	—	`exists_of_isLeft_left` `isLeft_congr`
`exists_of_isRight_left` 📖	—	—	—	—	—
`exists_of_isRight_right` 📖	—	—	—	—	`exists_of_isRight_left` `isRight_congr`
`isLeft_congr` 📖	—	—	—	—	—
`isLeft_left` 📖	—	—	—	—	—
`isLeft_right` 📖	—	—	—	—	—
`isRight_congr` 📖	—	—	—	—	—
`isRight_left` 📖	—	—	—	—	—
`isRight_right` 📖	—	—	—	—	—

Sum3

Definitions

Name	Category	Theorems
`in₀` 📖	CompOp	12 math math: `SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff'`, `SimpleGraph.TripartiteFromTriangles.rel_iff`, `SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff'`, `SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff`, `SimpleGraph.TripartiteFromTriangles.graph_triple`, `SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff`, `SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff'`, `SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff`, `SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff`, `SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff'`, `SimpleGraph.TripartiteFromTriangles.toTriangle_apply`, `SimpleGraph.TripartiteFromTriangles.Graph.not_in₀₀`
`in₁` 📖	CompOp	12 math math: `SimpleGraph.TripartiteFromTriangles.rel_iff`, `SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff'`, `SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff'`, `SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff`, `SimpleGraph.TripartiteFromTriangles.graph_triple`, `SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff'`, `SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff`, `SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff'`, `SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff`, `SimpleGraph.TripartiteFromTriangles.toTriangle_apply`, `SimpleGraph.TripartiteFromTriangles.Graph.not_in₁₁`, `SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff`
`in₂` 📖	CompOp	12 math math: `SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff'`, `SimpleGraph.TripartiteFromTriangles.rel_iff`, `SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff'`, `SimpleGraph.TripartiteFromTriangles.graph_triple`, `SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff`, `SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff'`, `SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff'`, `SimpleGraph.TripartiteFromTriangles.Graph.not_in₂₂`, `SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff`, `SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff`, `SimpleGraph.TripartiteFromTriangles.toTriangle_apply`, `SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff`

(root)

Theorems

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

---

← Back to Index