NAry

📁 Source: Mathlib/Order/Filter/NAry.lean

Statistics

Metric	Count
Definitions map₂	1
Theorems map₂, map₂, of_map₂_left, of_map₂_right, image2_mem_map₂, le_map₂_iff, map_map₂, map_map₂_antidistrib, map_map₂_antidistrib_left, map_map₂_antidistrib_right, map_map₂_distrib, map_map₂_distrib_left, map_map₂_distrib_right, map_map₂_right_anticomm, map_map₂_right_comm, map_prod_eq_map₂, map_prod_eq_map₂', map_uncurry_prod, neBot, map₂_assoc, map₂_bot_left, map₂_bot_right, map₂_comm, map₂_curry, map₂_distrib_le_left, map₂_distrib_le_right, map₂_eq_bot_iff, map₂_inf_subset_left, map₂_inf_subset_right, map₂_left, map₂_left_comm, map₂_left_identity, map₂_map_left, map₂_map_left_anticomm, map₂_map_left_comm, map₂_map_right, map₂_mk_eq_prod, map₂_mono, map₂_mono_left, map₂_mono_right, map₂_neBot_iff, map₂_pure, map₂_pure_left, map₂_pure_right, map₂_right, map₂_right_comm, map₂_right_identity, map₂_sup_left, map₂_sup_right, map₂_swap, mem_map₂_iff	51
Total	52

Filter

Definitions

Name	Category	Theorems
map₂ 📖	CompOp	56 math math: map_map₂_right_comm, map₂_bot_right, image2_mem_map₂, map_map₂_antidistrib_left, map₂_div, map₂_vsub, map₂_bot_left, map₂_neBot_iff, map₂_smul, map₂_map_right, map_map₂_distrib_left, map₂_map_left_anticomm, map₂_sup_right, map₂_distrib_le_left, map₂_distrib_le_right, map_prod_eq_map₂', map₂_right_identity, map₂_mono_right, map₂_map_left, mem_map₂_iff, map₂_comm, map₂_mk_eq_prod, map₂_vadd, le_map₂_iff, map₂_left_identity, map₂_pure_left, NeBot.map₂, map₂_left, map_map₂_distrib, map₂_right, map₂_assoc, HasBasis.map₂, map₂_mul, map_prod_eq_map₂, map₂_map_left_comm, map₂_mono, map₂.neBot, map_map₂_right_anticomm, map₂_sub, map_uncurry_prod, map₂_eq_bot_iff, map₂_pure, map₂_curry, map₂_swap, map₂_sup_left, map₂_add, map_map₂_antidistrib_right, map₂_pure_right, map_map₂_distrib_right, map₂_left_comm, map₂_mono_left, map_map₂_antidistrib, map_map₂, map₂_inf_subset_right, map₂_inf_subset_left, map₂_right_comm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image2_mem_map₂ 📖	mathematical	Set Filter instMembership	map₂ Set.image2	—	Set.Subset.rfl
le_map₂_iff 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder map₂ Set instMembership Set.image2	—	image2_mem_map₂ mem_of_superset
map_map₂ 📖	mathematical	—	map map₂	—	map_prod_eq_map₂ map_map
map_map₂_antidistrib 📖	mathematical	—	map map₂	—	map₂_swap map_map₂_distrib
map_map₂_antidistrib_left 📖	mathematical	—	map map₂	—	map_map₂_antidistrib
map_map₂_antidistrib_right 📖	mathematical	—	map map₂	—	map_map₂_antidistrib
map_map₂_distrib 📖	mathematical	—	map map₂	—	map_map₂ map₂_map_left map₂_map_right
map_map₂_distrib_left 📖	mathematical	—	map map₂	—	map_map₂_distrib
map_map₂_distrib_right 📖	mathematical	—	map map₂	—	map_map₂_distrib
map_map₂_right_anticomm 📖	mathematical	—	map₂ map	—	map_map₂_antidistrib_right
map_map₂_right_comm 📖	mathematical	—	map₂ map	—	map_map₂_distrib_right
map_prod_eq_map₂ 📖	mathematical	—	map SProd.sprod Filter instSProd map₂	—	map₂.eq_1 copy_eq Function.uncurry_def
map_prod_eq_map₂' 📖	mathematical	—	map SProd.sprod Filter instSProd map₂	—	map_prod_eq_map₂
map_uncurry_prod 📖	mathematical	—	map SProd.sprod Filter instSProd map₂	—	map₂_curry
map₂_assoc 📖	mathematical	—	map₂	—	map_prod_eq_map₂ map₂_map_left map₂_map_right prod_assoc map_map
map₂_bot_left 📖	mathematical	—	map₂ Bot.bot Filter instBot	—	map₂_eq_bot_iff
map₂_bot_right 📖	mathematical	—	map₂ Bot.bot Filter instBot	—	map₂_eq_bot_iff
map₂_comm 📖	mathematical	—	map₂	—	map₂_swap
map₂_curry 📖	mathematical	—	map₂ map SProd.sprod Filter instSProd	—	map_prod_eq_map₂'
map₂_distrib_le_left 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder map₂	—	inter_mem image2_mem_map₂ HasSubset.Subset.trans Set.instIsTransSubset Set.image2_distrib_subset_left Set.image2_subset Set.image2_subset_right Set.inter_subset_left Set.inter_subset_right
map₂_distrib_le_right 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder map₂	—	image2_mem_map₂ inter_mem HasSubset.Subset.trans Set.instIsTransSubset Set.image2_distrib_subset_right Set.image2_subset Set.image2_subset_left Set.inter_subset_left Set.inter_subset_right
map₂_eq_bot_iff 📖	mathematical	—	map₂ Bot.bot Filter instBot	—	—
map₂_inf_subset_left 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder map₂ instInf	—	Monotone.map_inf_le map₂_mono_right
map₂_inf_subset_right 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder map₂ instInf	—	Monotone.map_inf_le map₂_mono_left
map₂_left 📖	mathematical	—	map₂	—	map_prod_eq_map₂ map_fst_prod
map₂_left_comm 📖	mathematical	—	map₂	—	map₂_swap map₂_assoc
map₂_left_identity 📖	mathematical	—	map₂ Filter instPure	—	map₂_pure_left map_id
map₂_map_left 📖	mathematical	—	map₂ map	—	map_prod_eq_map₂ map_id prod_map_map_eq map_map
map₂_map_left_anticomm 📖	mathematical	—	map₂ map	—	map_map₂_antidistrib_left
map₂_map_left_comm 📖	mathematical	—	map₂ map	—	map_map₂_distrib_left
map₂_map_right 📖	mathematical	—	map₂ map	—	map₂_swap map₂_map_left
map₂_mk_eq_prod 📖	mathematical	—	map₂ SProd.sprod Filter instSProd	—	map_id'
map₂_mono 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder	map₂	—	—
map₂_mono_left 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder	map₂	—	map₂_mono Set.Subset.rfl
map₂_mono_right 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder	map₂	—	map₂_mono Set.Subset.rfl
map₂_neBot_iff 📖	mathematical	—	NeBot map₂	—	—
map₂_pure 📖	mathematical	—	map₂ Filter instPure	—	map₂_pure_right map_pure
map₂_pure_left 📖	mathematical	—	map₂ Filter instPure map	—	map_prod_eq_map₂ pure_prod map_map
map₂_pure_right 📖	mathematical	—	map₂ Filter instPure map	—	map_prod_eq_map₂ prod_pure map_map
map₂_right 📖	mathematical	—	map₂	—	map₂_swap map₂_left
map₂_right_comm 📖	mathematical	—	map₂	—	map₂_swap map₂_assoc
map₂_right_identity 📖	mathematical	—	map₂ Filter instPure	—	map₂_pure_right map_id'
map₂_sup_left 📖	mathematical	—	map₂ Filter instSup	—	sup_prod map_sup
map₂_sup_right 📖	mathematical	—	map₂ Filter instSup	—	prod_sup map_sup
map₂_swap 📖	mathematical	—	map₂	—	map_prod_eq_map₂ prod_comm map_map
mem_map₂_iff 📖	mathematical	—	Set Filter instMembership map₂ Set.instHasSubset Set.image2	—	—

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map₂ 📖	mathematical	Filter.HasBasis	Filter.map₂ Set.image2	—	map prod

Filter.NeBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map₂ 📖	mathematical	—	Filter.NeBot Filter.map₂	—	Filter.map₂_neBot_iff
of_map₂_left 📖	mathematical	—	Filter.NeBot	—	Filter.map₂_neBot_iff
of_map₂_right 📖	mathematical	—	Filter.NeBot	—	Filter.map₂_neBot_iff

Filter.map₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
neBot 📖	mathematical	—	Filter.NeBot Filter.map₂	—	Filter.NeBot.map₂

---

← Back to Index