Prod

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

Statistics

Metric	Count
Definitions	0
Theorems `curry`, `diag_of_prod`, `diag_of_prod_left`, `diag_of_prod_right`, `eventually_prod_of_eventually_swap`, `image_of_prod`, `prod_inl`, `prod_inr`, `prod_mk`, `trans_prod`, `prodMap`, `prodMap`, `of_curry`, `uncurry`, `prod`, `coprod_of_prod_top_left`, `coprod_of_prod_top_right`, `fst`, `prodMap`, `prodMap_coprod`, `prodMk`, `snd`, `bot_coprod`, `bot_coprod_bot`, `bot_prod`, `comap_prod`, `comap_prodMap_prod`, `compl_diagonal_mem_prod`, `compl_mem_coprod`, `coprod_bot`, `coprod_eq_prod_top_sup_top_prod`, `coprod_inf_prod_le`, `coprod_mono`, `coprod_neBot_iff`, `coprod_neBot_left`, `coprod_neBot_right`, `disjoint_prod`, `eventually_prod_iff`, `eventually_prod_principal_iff`, `eventually_swap_iff`, `frequently_prod_and`, `inf_prod`, `le_prod`, `le_prod_map_fst_snd`, `map_const_principal_coprod_map_id_principal`, `map_fst_prod`, `map_prod`, `map_prodMap_const_id_principal_coprod_principal`, `map_prodMap_coprod_le`, `map_pure_prod`, `map_snd_prod`, `map_swap4_prod`, `mem_coprod_iff`, `mem_prod_iff`, `mem_prod_iff_left`, `mem_prod_iff_right`, `mem_prod_principal`, `mem_prod_top`, `principal_coprod_principal`, `instNeBot`, `prod_assoc`, `prod_assoc_symm`, `prod_bot`, `prod_comap_comap_eq`, `prod_comm`, `prod_comm'`, `prod_eq`, `prod_eq_bot`, `prod_iInf_left`, `prod_iInf_right`, `prod_inf`, `prod_inf_prod`, `prod_inj`, `prod_le_prod`, `prod_map_left`, `prod_map_map_eq`, `prod_map_map_eq'`, `prod_map_right`, `prod_mem_prod`, `prod_mem_prod_iff`, `prod_mono`, `prod_mono_left`, `prod_mono_right`, `prod_neBot`, `prod_principal_principal`, `prod_pure`, `prod_pure_pure`, `prod_sup`, `prod_top`, `pure_prod`, `sup_prod`, `tendsto_diag`, `tendsto_fst`, `tendsto_prodAssoc`, `tendsto_prodAssoc_symm`, `tendsto_prod_iff`, `tendsto_prod_iff'`, `tendsto_prod_swap`, `tendsto_snd`, `tendsto_swap4_prod`, `top_prod`	101
Total	101

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_coprod` 📖	mathematical	—	`coprod` `Bot.bot` `Filter` `instBot` `comap`	—	`comap_bot` `sup_of_le_right`
`bot_coprod_bot` 📖	mathematical	—	`coprod` `Bot.bot` `Filter` `instBot`	—	`coprod_bot` `comap_bot`
`bot_prod` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `Bot.bot` `instBot`	—	`prod_eq_bot`
`comap_prod` 📖	mathematical	—	`comap` `SProd.sprod` `Filter` `instSProd` `instInf`	—	`prod_eq_inf` `comap_inf` `comap_comap`
`comap_prodMap_prod` 📖	mathematical	—	`comap` `SProd.sprod` `Filter` `instSProd`	—	`comap_inf` `comap_comap`
`compl_diagonal_mem_prod` 📖	mathematical	—	`Set` `Filter` `instMembership` `SProd.sprod` `instSProd` `Compl.compl` `Set.instCompl` `Set.diagonal` `Disjoint` `instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `instCompleteLatticeFilter`	—	—
`compl_mem_coprod` 📖	mathematical	—	`Set` `Filter` `instMembership` `coprod` `Compl.compl` `Set.instCompl` `Set.image`	—	—
`coprod_bot` 📖	mathematical	—	`coprod` `Bot.bot` `Filter` `instBot` `comap`	—	`comap_bot` `sup_of_le_left`
`coprod_eq_prod_top_sup_top_prod` 📖	mathematical	—	`coprod` `Filter` `instSup` `SProd.sprod` `instSProd` `Top.top` `instTop`	—	`prod_top` `top_prod`
`coprod_inf_prod_le` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instInf` `coprod` `SProd.sprod` `instSProd` `instSup`	—	`coprod_eq_prod_top_sup_top_prod` `inf_sup_right` `prod_inf_prod` `inf_of_le_right` `sup_le_sup` `prod_mono` `inf_le_left` `le_rfl`
`coprod_mono` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`coprod`	—	`sup_le_sup` `comap_mono`
`coprod_neBot_iff` 📖	mathematical	—	`NeBot` `coprod`	—	—
`coprod_neBot_left` 📖	mathematical	—	`NeBot` `coprod`	—	`coprod_neBot_iff`
`coprod_neBot_right` 📖	mathematical	—	`NeBot` `coprod`	—	`coprod_neBot_iff`
`disjoint_prod` 📖	mathematical	—	`Disjoint` `Filter` `instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `instCompleteLatticeFilter` `SProd.sprod` `instSProd`	—	`prod_inf_prod`
`eventually_prod_iff` 📖	mathematical	—	`Eventually` `SProd.sprod` `Filter` `instSProd`	—	`mem_prod_iff`
`eventually_prod_principal_iff` 📖	mathematical	—	`Eventually` `SProd.sprod` `Filter` `instSProd` `principal`	—	`eventually_iff` `mem_prod_principal`
`eventually_swap_iff` 📖	mathematical	—	`Eventually` `SProd.sprod` `Filter` `instSProd`	—	`prod_comm`
`frequently_prod_and` 📖	mathematical	—	`Frequently` `SProd.sprod` `Filter` `instSProd`	—	`prod_principal_principal`
`inf_prod` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `instInf`	—	`prod_inf_prod` `inf_idem`
`le_prod` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SProd.sprod` `instSProd` `Tendsto`	—	`tendsto_prod_iff'`
`le_prod_map_fst_snd` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SProd.sprod` `instSProd` `map`	—	`le_inf` `le_comap_map`
`map_const_principal_coprod_map_id_principal` 📖	mathematical	—	`coprod` `map` `principal` `Set` `Set.instSingletonSet` `Set.instUnion` `SProd.sprod` `Set.instSProd` `Set.univ`	—	`map_principal` `Set.image_singleton` `comap_principal` `Set.image_congr` `sup_principal` `Set.prod_univ` `Set.univ_prod`
`map_fst_prod` 📖	mathematical	—	`map` `SProd.sprod` `Filter` `instSProd`	—	`ext`
`map_prod` 📖	mathematical	—	`map` `SProd.sprod` `Filter` `instSProd` `seq`	—	—
`map_prodMap_const_id_principal_coprod_principal` 📖	mathematical	—	`map` `coprod` `principal` `Set` `Set.instSingletonSet` `SProd.sprod` `Set.instSProd` `Set.univ`	—	`principal_coprod_principal` `map_principal` `Set.ext`
`map_prodMap_coprod_le` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `coprod`	—	—
`map_pure_prod` 📖	mathematical	—	`map` `SProd.sprod` `Filter` `instSProd` `instPure`	—	`pure_prod`
`map_snd_prod` 📖	mathematical	—	`map` `SProd.sprod` `Filter` `instSProd`	—	`prod_comm` `map_map` `map_fst_prod`
`map_swap4_prod` 📖	mathematical	—	`map` `SProd.sprod` `Filter` `instSProd`	—	`map_swap4_eq_comap` `comap_inf` `comap_comap` `instAssociativeMin_mathlib` `instCommutativeMin_mathlib` `instIdempotentOpMin_mathlib`
`mem_coprod_iff` 📖	mathematical	—	`Set` `Filter` `instMembership` `coprod` `Set.instHasSubset` `Set.preimage`	—	—
`mem_prod_iff` 📖	mathematical	—	`Set` `Filter` `instMembership` `SProd.sprod` `instSProd` `Set.instHasSubset` `Set.instSProd`	—	`mem_inf_of_inter` `preimage_mem_comap`
`mem_prod_iff_left` 📖	mathematical	—	`Set` `Filter` `instMembership` `SProd.sprod` `instSProd` `Eventually`	—	`Iff.and` `forall₂_swap` `exists_mem_subset_iff`
`mem_prod_iff_right` 📖	mathematical	—	`Set` `Filter` `instMembership` `SProd.sprod` `instSProd` `Eventually`	—	`prod_comm` `mem_map` `mem_prod_iff_left`
`mem_prod_principal` 📖	mathematical	—	`Set` `Filter` `instMembership` `SProd.sprod` `instSProd` `principal` `setOf`	—	`exists_mem_subset_iff` `mem_prod_iff` `Iff.and` `Set.mk_mem_prod` `mem_principal_self`
`mem_prod_top` 📖	mathematical	—	`Set` `Filter` `instMembership` `SProd.sprod` `instSProd` `Top.top` `instTop` `setOf`	—	`principal_univ` `mem_prod_principal`
`principal_coprod_principal` 📖	mathematical	—	`coprod` `principal` `Compl.compl` `Set` `Set.instCompl` `SProd.sprod` `Set.instSProd`	—	`coprod.eq_1` `comap_principal` `sup_principal` `Set.prod_eq` `Set.compl_inter` `Set.preimage_compl` `compl_compl`
`prod_assoc` 📖	mathematical	—	`map` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.prodAssoc` `SProd.sprod` `Filter` `instSProd`	—	`comap_inf` `comap_comap` `inf_assoc`
`prod_assoc_symm` 📖	mathematical	—	`map` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Equiv.prodAssoc` `SProd.sprod` `Filter` `instSProd`	—	`map_equiv_symm` `comap_inf` `comap_comap` `inf_assoc`
`prod_bot` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `Bot.bot` `instBot`	—	`prod_eq_bot`
`prod_comap_comap_eq` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `comap`	—	`comap_comap` `comap_inf`
`prod_comm` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `map`	—	`prod_comm'` `map_swap_eq_comap_swap`
`prod_comm'` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `comap`	—	`comap_inf` `comap_comap` `inf_comm`
`prod_eq` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `seq` `map`	—	`map_prod`
`prod_eq_bot` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `Bot.bot` `instBot`	—	—
`prod_iInf_left` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `iInf` `instInfSet`	—	`comap_iInf` `iInf_inf`
`prod_iInf_right` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `iInf` `instInfSet`	—	`comap_iInf` `inf_iInf`
`prod_inf` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `instInf`	—	`prod_inf_prod` `inf_idem`
`prod_inf_prod` 📖	mathematical	—	`Filter` `instInf` `SProd.sprod` `instSProd`	—	`inf_left_comm` `inf_comm` `comap_inf` `inf_assoc`
`prod_inj` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd`	—	`prod_le_prod` `Eq.le` `LE.le.antisymm` `neBot_of_le` `Eq.ge`
`prod_le_prod` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SProd.sprod` `instSProd`	—	`Tendsto.mono_left` `tendsto_fst` `map_fst_prod` `tendsto_snd` `map_snd_prod` `prod_mono`
`prod_map_left` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `map`	—	`prod_map_map_eq'` `map_id`
`prod_map_map_eq` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `map`	—	`le_antisymm` `mem_prod_iff` `mem_of_superset` `prod_mem_prod` `image_mem_map` `Set.prod_image_image_eq` `Set.image_subset_iff` `Tendsto.prodMk` `Tendsto.comp` `tendsto_map` `tendsto_fst` `tendsto_snd`
`prod_map_map_eq'` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `map`	—	`prod_map_map_eq`
`prod_map_right` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `map`	—	`prod_map_map_eq'` `map_id`
`prod_mem_prod` 📖	mathematical	`Set` `Filter` `instMembership`	`SProd.sprod` `instSProd` `Set.instSProd`	—	`inter_mem_inf` `preimage_mem_comap`
`prod_mem_prod_iff` 📖	mathematical	—	`Set` `Filter` `instMembership` `SProd.sprod` `instSProd` `Set.instSProd`	—	`mem_prod_iff` `Set.prod_subset_prod_iff` `mem_of_superset` `Set.Nonempty.ne_empty` `nonempty_of_mem` `prod_mem_prod`
`prod_mono` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SProd.sprod` `instSProd`	—	`inf_le_inf` `comap_mono`
`prod_mono_left` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SProd.sprod` `instSProd`	—	`prod_mono` `Eq.le`
`prod_mono_right` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SProd.sprod` `instSProd`	—	`prod_mono` `Eq.le`
`prod_neBot` 📖	mathematical	—	`NeBot` `SProd.sprod` `Filter` `instSProd`	—	—
`prod_principal_principal` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `principal` `Set` `Set.instSProd`	—	`comap_principal` `inf_principal`
`prod_pure` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `instPure` `map`	—	`prod_eq` `seq_pure` `map_map`
`prod_pure_pure` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `instPure`	—	`prod_pure`
`prod_sup` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `instSup`	—	`comap_sup` `inf_sup_left`
`prod_top` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `Top.top` `instTop` `comap`	—	`prod_eq_inf` `comap_top` `inf_top_eq`
`pure_prod` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `instPure` `map`	—	`prod_eq` `map_pure` `pure_seq_eq_map`
`sup_prod` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `instSup`	—	`comap_sup` `inf_sup_right`
`tendsto_diag` 📖	mathematical	—	`Tendsto` `SProd.sprod` `Filter` `instSProd`	—	`tendsto_iff_eventually` `Eventually.diag_of_prod`
`tendsto_fst` 📖	mathematical	—	`Tendsto` `SProd.sprod` `Filter` `instSProd`	—	`tendsto_inf_left` `tendsto_comap`
`tendsto_prodAssoc` 📖	mathematical	—	`Tendsto` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.prodAssoc` `SProd.sprod` `Filter` `instSProd`	—	`Eq.le` `prod_assoc`
`tendsto_prodAssoc_symm` 📖	mathematical	—	`Tendsto` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Equiv.prodAssoc` `SProd.sprod` `Filter` `instSProd`	—	`Eq.le` `prod_assoc_symm`
`tendsto_prod_iff` 📖	mathematical	—	`Tendsto` `SProd.sprod` `Filter` `instSProd` `Set` `instMembership` `Set.instMembership`	—	—
`tendsto_prod_iff'` 📖	mathematical	—	`Tendsto` `SProd.sprod` `Filter` `instSProd`	—	—
`tendsto_prod_swap` 📖	mathematical	—	`Tendsto` `SProd.sprod` `Filter` `instSProd`	—	`Tendsto.prodMk` `tendsto_snd` `tendsto_fst`
`tendsto_snd` 📖	mathematical	—	`Tendsto` `SProd.sprod` `Filter` `instSProd`	—	`tendsto_inf_right` `tendsto_comap`
`tendsto_swap4_prod` 📖	mathematical	—	`Tendsto` `SProd.sprod` `Filter` `instSProd`	—	`Eq.le` `map_swap4_prod`
`top_prod` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `Top.top` `instTop` `comap`	—	`prod_eq_inf` `comap_top` `top_inf_eq`

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`curry` 📖	—	`Filter.Eventually` `SProd.sprod` `Filter` `Filter.instSProd`	—	—	`Filter.eventually_prod_iff` `mono`
`diag_of_prod` 📖	—	`Filter.Eventually` `SProd.sprod` `Filter` `Filter.instSProd`	—	—	`image_of_prod` `Filter.tendsto_id`
`diag_of_prod_left` 📖	—	`Filter.Eventually` `SProd.sprod` `Filter` `Filter.instSProd`	—	—	`Filter.eventually_prod_iff` `mono` `diag_of_prod`
`diag_of_prod_right` 📖	—	`Filter.Eventually` `SProd.sprod` `Filter` `Filter.instSProd`	—	—	`Filter.eventually_prod_iff` `mono` `diag_of_prod`
`eventually_prod_of_eventually_swap` 📖	mathematical	`Filter.Eventually`	`SProd.sprod` `Filter` `Filter.instSProd`	—	`Filter.eventually_prod_iff` `exists` `and`
`image_of_prod` 📖	—	`Filter.Tendsto` `Filter.Eventually` `SProd.sprod` `Filter` `Filter.instSProd`	—	—	`Filter.eventually_prod_iff` `Filter.mp_mem` `Filter.Tendsto.eventually` `Filter.univ_mem'`
`prod_inl` 📖	mathematical	`Filter.Eventually`	`SProd.sprod` `Filter` `Filter.instSProd`	—	`Filter.Tendsto.eventually` `Filter.tendsto_fst`
`prod_inr` 📖	mathematical	`Filter.Eventually`	`SProd.sprod` `Filter` `Filter.instSProd`	—	`Filter.Tendsto.eventually` `Filter.tendsto_snd`
`prod_mk` 📖	mathematical	`Filter.Eventually`	`SProd.sprod` `Filter` `Filter.instSProd`	—	`and` `prod_inl` `prod_inr`
`trans_prod` 📖	—	`Filter.Eventually` `SProd.sprod` `Filter` `Filter.instSProd`	—	—	`eventually_prod_of_eventually_swap` `curry` `Filter.eventually_swap_iff`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodMap` 📖	mathematical	`Filter.EventuallyEq`	`SProd.sprod` `Filter` `Filter.instSProd`	—	`Filter.Eventually.mono`

Filter.EventuallyLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodMap` 📖	mathematical	`Filter.EventuallyLE`	`Prod.instLE_mathlib` `SProd.sprod` `Filter` `Filter.instSProd`	—	—

Filter.Frequently

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_curry` 📖	mathematical	`Filter.Frequently`	`SProd.sprod` `Filter` `Filter.instSProd`	—	`uncurry`
`uncurry` 📖	mathematical	`Filter.Frequently`	`SProd.sprod` `Filter` `Filter.instSProd`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Filter.Eventually.curry`

Filter.NeBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	—	`Filter.NeBot` `SProd.sprod` `Filter` `Filter.instSProd`	—	`Filter.prod_neBot`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprod_of_prod_top_left` 📖	mathematical	`Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd` `Filter.principal` `Compl.compl` `Set` `Set.instCompl` `Top.top` `Filter.instTop`	`Filter.coprod`	—	`Filter.coprod_eq_prod_top_sup_top_prod`
`coprod_of_prod_top_right` 📖	mathematical	`Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd` `Filter.principal` `Compl.compl` `Set` `Set.instCompl` `Top.top` `Filter.instTop`	`Filter.coprod`	—	`Filter.coprod_eq_prod_top_sup_top_prod`
`fst` 📖	—	`Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd`	—	—	`comp` `Filter.tendsto_fst`
`prodMap` 📖	mathematical	`Filter.Tendsto`	`SProd.sprod` `Filter` `Filter.instSProd`	—	`eq_1` `Prod.map_def` `Filter.prod_map_map_eq` `Filter.prod_mono`
`prodMap_coprod` 📖	mathematical	`Filter.Tendsto`	`Filter.coprod`	—	`LE.le.trans` `Filter.map_prodMap_coprod_le` `Filter.coprod_mono`
`prodMk` 📖	mathematical	`Filter.Tendsto`	`SProd.sprod` `Filter` `Filter.instSProd`	—	`Filter.tendsto_inf` `Filter.tendsto_comap_iff`
`snd` 📖	—	`Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd`	—	—	`comp` `Filter.tendsto_snd`

Filter.prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNeBot` 📖	mathematical	—	`Filter.NeBot` `SProd.sprod` `Filter` `Filter.instSProd`	—	`Filter.NeBot.prod`

---

← Back to Index