NAry

📁 Source: Mathlib/Data/Set/NAry.lean

Statistics

Metric	Count
Definitions	0
Theorems `image2`, `of_image2_left`, `of_image2_right`, `image2`, `exists_mem_image2`, `forall_mem_image2`, `image2_assoc`, `image2_comm`, `image2_congr`, `image2_congr'`, `image2_curry`, `image2_distrib_subset_left`, `image2_distrib_subset_right`, `image2_empty_left`, `image2_empty_right`, `image2_eq_empty_iff`, `image2_image2_image2_comm`, `image2_image_left`, `image2_image_left_anticomm`, `image2_image_left_comm`, `image2_image_right`, `image2_insert_left`, `image2_insert_right`, `image2_inter_left`, `image2_inter_right`, `image2_inter_subset_left`, `image2_inter_subset_right`, `image2_inter_union_subset`, `image2_inter_union_subset_union`, `image2_left`, `image2_left_comm`, `image2_left_identity`, `image2_mk_eq_prod`, `image2_nonempty_iff`, `image2_range`, `image2_right`, `image2_right_comm`, `image2_right_identity`, `image2_singleton`, `image2_singleton_left`, `image2_singleton_right`, `image2_subset`, `image2_subset_iff`, `image2_subset_iff_left`, `image2_subset_iff_right`, `image2_subset_left`, `image2_subset_right`, `image2_swap`, `image2_union_inter_subset`, `image2_union_inter_subset_union`, `image2_union_left`, `image2_union_right`, `image_image2`, `image_image2_antidistrib`, `image_image2_antidistrib_left`, `image_image2_antidistrib_right`, `image_image2_distrib`, `image_image2_distrib_left`, `image_image2_distrib_right`, `image_image2_right_anticomm`, `image_image2_right_comm`, `image_prod`, `image_subset_image2_left`, `image_subset_image2_right`, `image_uncurry_prod`, `mem_image2_iff`, `subset_image2_diff_left`, `subset_image2_diff_right`	68
Total	68

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_image2` 📖	mathematical	—	`Set` `instMembership` `image2`	—	—
`forall_mem_image2` 📖	—	—	—	—	—
`image2_assoc` 📖	mathematical	—	`image2`	—	`eq_of_forall_subset_iff`
`image2_comm` 📖	mathematical	—	`image2`	—	`image2_swap` `image2_congr`
`image2_congr` 📖	mathematical	—	`image2`	—	—
`image2_congr'` 📖	mathematical	—	`image2`	—	`image2_congr`
`image2_curry` 📖	mathematical	—	`image2` `image` `SProd.sprod` `Set` `instSProd`	—	`image_congr`
`image2_distrib_subset_left` 📖	mathematical	—	`Set` `instHasSubset` `image2`	—	—
`image2_distrib_subset_right` 📖	mathematical	—	`Set` `instHasSubset` `image2`	—	—
`image2_empty_left` 📖	mathematical	—	`image2` `Set` `instEmptyCollection`	—	`ext`
`image2_empty_right` 📖	mathematical	—	`image2` `Set` `instEmptyCollection`	—	`ext`
`image2_eq_empty_iff` 📖	mathematical	—	`image2` `Set` `instEmptyCollection`	—	`not_nonempty_iff_eq_empty` `image2_nonempty_iff` `not_and_or`
`image2_image2_image2_comm` 📖	mathematical	—	`image2`	—	—
`image2_image_left` 📖	mathematical	—	`image2` `image`	—	`ext`
`image2_image_left_anticomm` 📖	mathematical	—	`image2` `image`	—	`image_image2_antidistrib_left`
`image2_image_left_comm` 📖	mathematical	—	`image2` `image`	—	`image_image2_distrib_left`
`image2_image_right` 📖	mathematical	—	`image2` `image`	—	`ext`
`image2_insert_left` 📖	mathematical	—	`image2` `Set` `instInsert` `instUnion` `image`	—	`insert_eq` `image2_union_left` `image2_singleton_left`
`image2_insert_right` 📖	mathematical	—	`image2` `Set` `instInsert` `instUnion` `image`	—	`insert_eq` `image2_union_right` `image2_singleton_right`
`image2_inter_left` 📖	mathematical	`Function.Injective2`	`image2` `Set` `instInter`	—	`inter_prod` `image_inter` `Function.Injective2.uncurry`
`image2_inter_right` 📖	mathematical	`Function.Injective2`	`image2` `Set` `instInter`	—	`prod_inter` `image_inter` `Function.Injective2.uncurry`
`image2_inter_subset_left` 📖	mathematical	—	`Set` `instHasSubset` `image2` `instInter`	—	`Monotone.map_inf_le` `image2_subset_right`
`image2_inter_subset_right` 📖	mathematical	—	`Set` `instHasSubset` `image2` `instInter`	—	`Monotone.map_inf_le` `image2_subset_left`
`image2_inter_union_subset` 📖	mathematical	—	`Set` `instHasSubset` `image2` `instInter` `instUnion`	—	`inter_comm` `HasSubset.Subset.trans` `instIsTransSubset` `image2_inter_union_subset_union` `union_subset` `Eq.subset` `instReflSubset` `image2_comm` `Subset.rfl`
`image2_inter_union_subset_union` 📖	mathematical	—	`Set` `instHasSubset` `image2` `instInter` `instUnion`	—	`image2_union_right` `union_subset_union` `image2_subset_right` `inter_subset_left` `inter_subset_right`
`image2_left` 📖	mathematical	`Nonempty`	`image2`	—	`nonempty_def`
`image2_left_comm` 📖	mathematical	—	`image2`	—	`image2_swap` `image2_assoc`
`image2_left_identity` 📖	mathematical	—	`image2` `Set` `instSingletonSet`	—	`image2_singleton_left` `image_id`
`image2_mk_eq_prod` 📖	mathematical	—	`image2` `SProd.sprod` `Set` `instSProd`	—	`ext`
`image2_nonempty_iff` 📖	mathematical	—	`Nonempty` `image2`	—	`Nonempty.image2`
`image2_range` 📖	mathematical	—	`image2` `range`	—	`image2_image_left` `image2_image_right` `univ_prod_univ`
`image2_right` 📖	mathematical	`Nonempty`	`image2`	—	`nonempty_def`
`image2_right_comm` 📖	mathematical	—	`image2`	—	`image2_swap` `image2_assoc`
`image2_right_identity` 📖	mathematical	—	`image2` `Set` `instSingletonSet`	—	`image2_singleton_right` `image_id'`
`image2_singleton` 📖	mathematical	—	`image2` `Set` `instSingletonSet`	—	`image2_singleton_right` `image_singleton`
`image2_singleton_left` 📖	mathematical	—	`image2` `Set` `instSingletonSet` `image`	—	`ext`
`image2_singleton_right` 📖	mathematical	—	`image2` `Set` `instSingletonSet` `image`	—	`ext`
`image2_subset` 📖	mathematical	`Set` `instHasSubset`	`image2`	—	`mem_image2_of_mem`
`image2_subset_iff` 📖	mathematical	—	`Set` `instHasSubset` `image2` `instMembership`	—	`forall_mem_image2`
`image2_subset_iff_left` 📖	mathematical	—	`Set` `instHasSubset` `image2` `image`	—	—
`image2_subset_iff_right` 📖	mathematical	—	`Set` `instHasSubset` `image2` `image`	—	`forall₂_swap`
`image2_subset_left` 📖	mathematical	`Set` `instHasSubset`	`image2`	—	`image2_subset` `Subset.rfl`
`image2_subset_right` 📖	mathematical	`Set` `instHasSubset`	`image2`	—	`image2_subset` `Subset.rfl`
`image2_swap` 📖	mathematical	—	`image2`	—	—
`image2_union_inter_subset` 📖	mathematical	—	`Set` `instHasSubset` `image2` `instUnion` `instInter`	—	`image2_comm` `image2_inter_union_subset`
`image2_union_inter_subset_union` 📖	mathematical	—	`Set` `instHasSubset` `image2` `instUnion` `instInter`	—	`image2_union_left` `union_subset_union` `image2_subset_left` `inter_subset_left` `inter_subset_right`
`image2_union_left` 📖	mathematical	—	`image2` `Set` `instUnion`	—	`union_prod` `image_union`
`image2_union_right` 📖	mathematical	—	`image2` `Set` `instUnion`	—	`image2_swap` `image2_union_left`
`image_image2` 📖	mathematical	—	`image` `image2`	—	`image_image`
`image_image2_antidistrib` 📖	mathematical	—	`image` `image2`	—	`image2_swap` `image_image2_distrib`
`image_image2_antidistrib_left` 📖	mathematical	—	`image` `image2`	—	`image_image2_antidistrib` `image_id'`
`image_image2_antidistrib_right` 📖	mathematical	—	`image` `image2`	—	`image_image2_antidistrib` `image_id'`
`image_image2_distrib` 📖	mathematical	—	`image` `image2`	—	`image_image2` `image2_image_left` `image2_image_right` `image2_congr`
`image_image2_distrib_left` 📖	mathematical	—	`image` `image2`	—	`image_image2_distrib` `image_id'`
`image_image2_distrib_right` 📖	mathematical	—	`image` `image2`	—	`image_image2_distrib` `image_id'`
`image_image2_right_anticomm` 📖	mathematical	—	`image2` `image`	—	`image_image2_antidistrib_right`
`image_image2_right_comm` 📖	mathematical	—	`image2` `image`	—	`image_image2_distrib_right`
`image_prod` 📖	mathematical	—	`image` `SProd.sprod` `Set` `instSProd` `image2`	—	`ext`
`image_subset_image2_left` 📖	mathematical	`Set` `instMembership`	`instHasSubset` `image` `image2`	—	`forall_mem_image` `mem_image2_of_mem`
`image_subset_image2_right` 📖	mathematical	`Set` `instMembership`	`instHasSubset` `image` `image2`	—	`forall_mem_image` `mem_image2_of_mem`
`image_uncurry_prod` 📖	mathematical	—	`image` `SProd.sprod` `Set` `instSProd` `image2`	—	`image_prod`
`mem_image2_iff` 📖	mathematical	`Function.Injective2`	`Set` `instMembership` `image2`	—	`mem_image2_of_mem`
`subset_image2_diff_left` 📖	mathematical	—	`Set` `instHasSubset` `instSDiff` `image2`	—	—
`subset_image2_diff_right` 📖	mathematical	—	`Set` `instHasSubset` `instSDiff` `image2`	—	—

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image2` 📖	mathematical	`Set.Nonempty`	`Set.image2`	—	`Set.mem_image2_of_mem`
`of_image2_left` 📖	—	`Set.Nonempty` `Set.image2`	—	—	`Set.image2_nonempty_iff`
`of_image2_right` 📖	—	`Set.Nonempty` `Set.image2`	—	—	`Set.image2_nonempty_iff`

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image2` 📖	mathematical	`Set.Subsingleton`	`Set.image2`	—	`Set.image_prod` `image` `prod`

---

← Back to Index