Pointwise

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

Statistics

Metric	Count
Definitions `addAction`, `addActionFilter`, `addCommMonoid`, `addCommSemigroup`, `addMonoid`, `addSemigroup`, `addZeroClass`, `commMonoid`, `commSemigroup`, `distribMulActionFilter`, `divisionCommMonoid`, `divisionMonoid`, `instAdd`, `instDistribNeg`, `instDiv`, `instInv`, `instInvolutiveInv`, `instInvolutiveNeg`, `instMul`, `instNPow`, `instNSMul`, `instNeg`, `instOne`, `instSMul`, `instSMulFilter`, `instSub`, `instVAdd`, `instVAddFilter`, `instVSub`, `instZPow`, `instZSMul`, `instZero`, `mapAddMonoidHom`, `mapMonoidHom`, `monoid`, `mulAction`, `mulActionFilter`, `mulDistribMulActionFilter`, `mulOneClass`, `pureAddHom`, `pureAddMonoidHom`, `pureMonoidHom`, `pureMulHom`, `pureOneHom`, `pureZeroHom`, `semigroup`, `subtractionCommMonoid`, `subtractionMonoid`	48
Theorems `add`, `div`, `inv`, `mul`, `neg`, `smul`, `sub`, `vadd`, `add`, `div`, `div_zero_nonneg`, `inv`, `le_one_iff`, `mul`, `mul_zero_nonneg`, `neg`, `nonneg_sub`, `nonpos_iff`, `of_add_left`, `of_add_right`, `of_div_left`, `of_div_right`, `of_mul_left`, `of_mul_right`, `of_smul_filter`, `of_smul_left`, `of_smul_right`, `of_sub_left`, `of_sub_right`, `of_vadd_filter`, `of_vadd_left`, `of_vadd_right`, `of_vsub_left`, `of_vsub_right`, `one_le_div`, `smul`, `smul_filter`, `smul_zero_nonneg`, `sub`, `vadd`, `vadd_filter`, `vsub`, `zero_div_nonneg`, `zero_mul_nonneg`, `zero_smul_nonneg`, `add_add`, `div_div`, `inv_inv`, `mul_mul`, `neg_neg`, `sub_sub`, `instNeBot`, `addLeftMono`, `addRightMono`, `add_bot`, `add_eq_bot_iff`, `add_eq_zero_iff`, `add_mem_add`, `add_mul_subset`, `add_neBot_iff`, `add_pure`, `add_top_of_nonneg`, `bot_add`, `bot_div`, `bot_mul`, `bot_pow`, `bot_smul`, `bot_sub`, `bot_vadd`, `bot_vsub`, `coe_pureAddHom`, `coe_pureAddMonoidHom`, `coe_pureMonoidHom`, `coe_pureMulHom`, `coe_pureOneHom`, `coe_pureZeroHom`, `comap_add_comap_le`, `comap_inv`, `comap_mul_comap_le`, `comap_neg`, `covariant_div`, `covariant_smul`, `covariant_smul_filter`, `covariant_sub`, `covariant_swap_div`, `covariant_swap_sub`, `covariant_vadd`, `covariant_vadd_filter`, `instNeBot`, `div_bot`, `div_eq_bot_iff`, `div_le_div`, `div_le_div_left`, `div_le_div_right`, `div_mem_div`, `div_neBot_iff`, `div_pure`, `eventually_one`, `eventually_zero`, `instNeBot`, `inv_atTop`, `inv_eq_bot_iff`, `inv_le_iff_le_inv`, `inv_le_inv`, `inv_le_inv_iff`, `inv_le_self`, `inv_mem_inv`, `inv_pure`, `isAddUnit_iff`, `isAddUnit_pure`, `isCentralScalar`, `isCentralVAdd`, `isScalarTower`, `isScalarTower'`, `isScalarTower''`, `isUnit_iff`, `isUnit_iff_singleton`, `isUnit_pure`, `le_add_iff`, `le_div_iff`, `le_mul_iff`, `le_one_iff`, `le_smul_iff`, `le_sub_iff`, `le_vadd_iff`, `le_vsub_iff`, `map_add`, `map_div`, `map_inv`, `map_inv'`, `map_mul`, `map_neg`, `map_neg'`, `map_one`, `map_one'`, `map_smul`, `map_sub`, `map_vadd`, `map_zero`, `map_zero'`, `map₂_add`, `map₂_div`, `map₂_mul`, `map₂_smul`, `map₂_sub`, `map₂_vadd`, `map₂_vsub`, `mem_add`, `mem_div`, `mem_inv`, `mem_mul`, `mem_neg`, `mem_one`, `mem_smul`, `mem_smul_filter`, `mem_sub`, `mem_vadd`, `mem_vadd_filter`, `mem_vsub`, `mem_zero`, `instNeBot`, `mulLeftMono`, `mulRightMono`, `mul_add_subset`, `mul_bot`, `mul_eq_bot_iff`, `mul_eq_one_iff`, `mul_mem_mul`, `mul_neBot_iff`, `mul_pure`, `mul_top_of_one_le`, `neBot_inv_iff`, `neBot_neg_iff`, `instNeBot`, `neg_atTop`, `neg_eq_bot_iff`, `neg_le_iff_le_neg`, `neg_le_neg`, `neg_le_neg_iff`, `neg_le_self`, `neg_mem_neg`, `neg_pure`, `nonneg_sub_iff`, `nonpos_iff`, `not_nonneg_sub_iff`, `not_one_le_div_iff`, `nsmul_bot`, `nsmul_mem_nsmul`, `nsmul_top`, `one_le_div_iff`, `one_mem_one`, `one_neBot`, `one_prod`, `one_prod_one`, `pow_mem_pow`, `principal_one`, `principal_zero`, `prod_one`, `prod_zero`, `pureAddHom_apply`, `pureAddMonoidHom_apply`, `pureMonoidHom_apply`, `pureMulHom_apply`, `pureOneHom_apply`, `pureZeroHom_apply`, `pure_add`, `pure_add_pure`, `pure_div`, `pure_div_pure`, `pure_mul`, `pure_mul_pure`, `pure_one`, `pure_smul`, `pure_smul_pure`, `pure_sub`, `pure_sub_pure`, `pure_vadd`, `pure_vadd_pure`, `pure_vsub`, `pure_vsub_pure`, `pure_zero`, `instNeBot`, `smulCommClass`, `smulCommClass_filter`, `smulCommClass_filter'`, `smulCommClass_filter''`, `smul_bot`, `smul_eq_bot_iff`, `instNeBot`, `smul_filter_bot`, `smul_filter_eq_bot_iff`, `smul_filter_le_smul_filter`, `smul_filter_neBot_iff`, `smul_le_smul`, `smul_le_smul_left`, `smul_le_smul_right`, `smul_mem_smul`, `smul_neBot_iff`, `smul_pure`, `smul_set_mem_smul_filter`, `smul_tendsto_smul_iff`, `smul_tendsto_smul_iff₀`, `instNeBot`, `sub_bot`, `sub_eq_bot_iff`, `sub_le_sub`, `sub_le_sub_left`, `sub_le_sub_right`, `sub_mem_sub`, `sub_neBot_iff`, `sub_pure`, `tendsto_one`, `tendsto_zero`, `top_add_of_nonneg`, `top_add_top`, `top_mul_of_one_le`, `top_mul_top`, `top_pow`, `instNeBot`, `vaddAssocClass`, `vaddAssocClass'`, `vaddAssocClass''`, `vaddCommClass`, `vaddCommClass_filter`, `vaddCommClass_filter'`, `vaddCommClass_filter''`, `vadd_bot`, `vadd_eq_bot_iff`, `instNeBot`, `vadd_filter_bot`, `vadd_filter_eq_bot_iff`, `vadd_filter_le_vadd_filter`, `vadd_filter_neBot_iff`, `vadd_le_vadd`, `vadd_le_vadd_left`, `vadd_le_vadd_right`, `vadd_mem_vadd`, `vadd_neBot_iff`, `vadd_pure`, `vadd_set_mem_vadd_filter`, `vadd_tendsto_vadd_iff`, `instNeBot`, `vsub_bot`, `vsub_eq_bot_iff`, `vsub_le_vsub`, `vsub_le_vsub_left`, `vsub_le_vsub_right`, `vsub_mem_vsub`, `vsub_neBot_iff`, `vsub_pure`, `zero_mem_zero`, `zero_neBot`, `zero_prod`, `zero_prod_zero`, `zero_smul_filter`, `zero_smul_filter_nonpos`, `filter`, `vadd_tendsto_vadd_iff`, `filter`, `smul_tendsto_smul_iff`	300
Total	348

Filter

Definitions

Name	Category	Theorems
`addAction` 📖	CompOp	—
`addActionFilter` 📖	CompOp	—
`addCommMonoid` 📖	CompOp	—
`addCommSemigroup` 📖	CompOp	—
`addMonoid` 📖	CompOp	3 math math: `IsAddUnit.filter`, `isAddUnit_iff`, `isAddUnit_pure`
`addSemigroup` 📖	CompOp	—
`addZeroClass` 📖	CompOp	2 math math: `pureAddMonoidHom_apply`, `coe_pureAddMonoidHom`
`commMonoid` 📖	CompOp	—
`commSemigroup` 📖	CompOp	—
`distribMulActionFilter` 📖	CompOp	—
`divisionCommMonoid` 📖	CompOp	—
`divisionMonoid` 📖	CompOp	—
`instAdd` 📖	CompOp	32 math math: `top_add_top`, `add_pure`, `map_add`, `add_eq_zero_iff`, `HasBasis.add`, `nhds_add_nhds_zero`, `addRightMono`, `top_add_of_nonneg`, `add_eq_bot_iff`, `le_add_iff`, `add_top_of_nonneg`, `addLeftMono`, `le_nhds_add`, `nhds_add`, `nhds_zero_add_nhds`, `Tendsto.add_add`, `pure_add`, `add.instNeBot`, `add_mem_add`, `NeBot.add`, `add_neBot_iff`, `mul_add_subset`, `nhdsAddHom_apply`, `add_mul_subset`, `pureAddHom_apply`, `map₂_add`, `bot_add`, `mem_add`, `comap_add_comap_le`, `pure_add_pure`, `coe_pureAddHom`, `add_bot`
`instDistribNeg` 📖	CompOp	—
`instDiv` 📖	CompOp	26 math math: `map₂_div`, `NeBot.zero_div_nonneg`, `covariant_div`, `div_mem_div`, `div_eq_bot_iff`, `pure_div`, `div_neBot_iff`, `covariant_swap_div`, `div_le_div`, `div.instNeBot`, `div_le_div_left`, `not_one_le_div_iff`, `le_div_iff`, `div_le_div_right`, `div_bot`, `bot_div`, `one_le_div_iff`, `div_pure`, `mem_div`, `HasBasis.div`, `Tendsto.div_div`, `map_div`, `NeBot.one_le_div`, `NeBot.div`, `NeBot.div_zero_nonneg`, `pure_div_pure`
`instInv` 📖	CompOp	31 math math: `inv_le_inv_iff`, `inv_atBot₀`, `inv_nhdsWithin_ne_zero`, `map_inv`, `inv_atTop₀`, `inv_nhdsNE_zero`, `inv_atTop`, `map_inv'`, `inv_nhdsGT`, `mem_inv`, `MeasureTheory.inv_ae`, `inv_cobounded₀`, `inv_nhdsNE`, `inv_nhdsLT`, `inv_nhdsGT_zero`, `inv_le_inv`, `NeBot.inv`, `nhds_inv₀`, `Tendsto.inv_inv`, `inv.instNeBot`, `HasBasis.inv`, `inv_nhdsLT_zero`, `comap_inv`, `inv_eq_bot_iff`, `inv_mem_inv`, `neBot_inv_iff`, `nhds_inv`, `inv_pure`, `inv_le_self`, `inv_cobounded`, `inv_le_iff_le_inv`
`instInvolutiveInv` 📖	CompOp	—
`instInvolutiveNeg` 📖	CompOp	—
`instMul` 📖	CompOp	34 math math: `map_mul`, `bot_mul`, `nhds_mul_nhds_one`, `pure_mul`, `mul_mem_mul`, `mem_mul`, `le_mul_iff`, `pure_mul_pure`, `NeBot.mul`, `NeBot.zero_mul_nonneg`, `mul_pure`, `top_mul_top`, `mulLeftMono`, `comap_mul_comap_le`, `mul_eq_bot_iff`, `map₂_mul`, `mul.instNeBot`, `coe_pureMulHom`, `NeBot.mul_zero_nonneg`, `mul_add_subset`, `nhds_mul`, `top_mul_of_one_le`, `mul_bot`, `pureMulHom_apply`, `add_mul_subset`, `mul_neBot_iff`, `mul_eq_one_iff`, `mul_top_of_one_le`, `le_nhds_mul`, `nhds_one_mul_nhds`, `mulRightMono`, `Tendsto.mul_mul`, `nhdsMulHom_apply`, `HasBasis.mul`
`instNPow` 📖	CompOp	3 math math: `top_pow`, `pow_mem_pow`, `bot_pow`
`instNSMul` 📖	CompOp	3 math math: `nsmul_mem_nsmul`, `nsmul_bot`, `nsmul_top`
`instNeg` 📖	CompOp	23 math math: `neg_atTop`, `comap_neg`, `neg_le_self`, `map_neg`, `neBot_neg_iff`, `neg_mem_neg`, `nhds_neg`, `map_neg'`, `neg_nhdsGT`, `neg_nhdsLT`, `neg_le_neg`, `neg_nhdsNE`, `neg_pure`, `Tendsto.neg_neg`, `neg_eq_bot_iff`, `MeasureTheory.neg_ae`, `neg_cobounded`, `mem_neg`, `neg_le_iff_le_neg`, `HasBasis.neg`, `neg.instNeBot`, `NeBot.neg`, `neg_le_neg_iff`
`instOne` 📖	CompOp	21 math math: `one_prod_one`, `one_le_nhds_iff`, `tendsto_one`, `mem_one`, `le_one_iff`, `one_mem_one`, `map_one'`, `NeBot.le_one_iff`, `pureOneHom_apply`, `prod_one`, `not_one_le_div_iff`, `eventually_one`, `pure_one`, `one_le_div_iff`, `coe_pureOneHom`, `mul_eq_one_iff`, `principal_one`, `one_neBot`, `one_prod`, `map_one`, `NeBot.one_le_div`
`instSMul` 📖	CompOp	29 math math: `le_smul_iff`, `smulCommClass`, `bot_smul`, `smul_mem_smul`, `map₂_smul`, `NeBot.zero_smul_nonneg`, `NeBot.smul_zero_nonneg`, `smul_pure`, `smulCommClass_filter''`, `mem_smul`, `smul_neBot_iff`, `pure_smul`, `smul_eq_bot_iff`, `top_smul_nhds_zero`, `tangentConeAt_def`, `HasBasis.smul`, `smul_bot`, `pure_smul_pure`, `smulCommClass_filter'`, `NeBot.smul`, `covariant_smul`, `isScalarTower''`, `smul.instNeBot`, `smul_le_smul_right`, `AffineSpace.asymptoticNhds_eq_smul`, `smul_le_smul`, `AffineSpace.asymptoticNhds_eq_smul_vadd`, `smul_le_smul_left`, `isScalarTower'`
`instSMulFilter` 📖	CompOp	29 math math: `smul_tendsto_smul_iff₀`, `punctured_nhds_smul`, `smul_filter.instNeBot`, `isCentralScalar`, `smul_uniformity₀`, `zero_smul_filter_nonpos`, `nhds_smul₀`, `smulCommClass_filter''`, `smulCommClass_filter`, `zero_smul_filter`, `MeasureTheory.smul_ae`, `isScalarTower`, `smul_filter_eq_bot_iff`, `smul_filter_le_smul_filter`, `smulCommClass_filter'`, `IsUnit.smul_uniformity`, `punctured_nhds_smul₀`, `IsUnit.smul_tendsto_smul_iff`, `map_smul`, `smul_uniformity`, `smul_tendsto_smul_iff`, `NeBot.smul_filter`, `smul_filter_neBot_iff`, `mem_smul_filter`, `smul_set_mem_smul_filter`, `covariant_smul_filter`, `isScalarTower'`, `nhds_smul`, `smul_filter_bot`
`instSub` 📖	CompOp	24 math math: `bot_sub`, `sub.instNeBot`, `le_sub_iff`, `mem_sub`, `pure_sub_pure`, `map_sub`, `not_nonneg_sub_iff`, `sub_neBot_iff`, `sub_le_sub`, `pure_sub`, `nonneg_sub_iff`, `NeBot.sub`, `Tendsto.sub_sub`, `sub_pure`, `sub_le_sub_right`, `covariant_sub`, `map₂_sub`, `sub_mem_sub`, `sub_bot`, `HasBasis.sub`, `sub_le_sub_left`, `NeBot.nonneg_sub`, `sub_eq_bot_iff`, `covariant_swap_sub`
`instVAdd` 📖	CompOp	25 math math: `vadd_le_vadd`, `mem_vadd`, `vaddCommClass_filter''`, `pure_vadd_pure`, `vaddAssocClass''`, `vadd_mem_vadd`, `bot_vadd`, `vadd_neBot_iff`, `AffineSpace.asymptoticNhds_vadd_pure`, `map₂_vadd`, `vadd_le_vadd_left`, `vadd_pure`, `vadd_le_vadd_right`, `HasBasis.vadd`, `NeBot.vadd`, `vaddCommClass`, `covariant_vadd`, `vadd_bot`, `vadd_eq_bot_iff`, `vadd.instNeBot`, `le_vadd_iff`, `AffineSpace.asymptoticNhds_eq_smul_vadd`, `vaddAssocClass'`, `vaddCommClass_filter'`, `pure_vadd`
`instVAddFilter` 📖	CompOp	24 math math: `MeasureTheory.vadd_ae`, `vaddCommClass_filter''`, `nhds_vadd`, `vaddAssocClass`, `vadd_tendsto_vadd_iff`, `NeBot.vadd_filter`, `IsAddUnit.vadd_tendsto_vadd_iff`, `isCentralVAdd`, `AffineSpace.vadd_asymptoticNhds`, `vaddCommClass_filter`, `vadd_filter_bot`, `vadd_filter_le_vadd_filter`, `mem_vadd_filter`, `vadd_uniformity`, `covariant_vadd_filter`, `vadd_filter_neBot_iff`, `IsAddUnit.vadd_uniformity`, `vadd_filter_eq_bot_iff`, `punctured_nhds_vadd`, `vadd_filter.instNeBot`, `map_vadd`, `vadd_set_mem_vadd_filter`, `vaddAssocClass'`, `vaddCommClass_filter'`
`instVSub` 📖	CompOp	16 math math: `NeBot.vsub`, `vsub.instNeBot`, `map₂_vsub`, `vsub_le_vsub_left`, `bot_vsub`, `vsub_bot`, `vsub_eq_bot_iff`, `le_vsub_iff`, `pure_vsub_pure`, `mem_vsub`, `vsub_pure`, `pure_vsub`, `vsub_neBot_iff`, `vsub_le_vsub_right`, `vsub_le_vsub`, `vsub_mem_vsub`
`instZPow` 📖	CompOp	—
`instZSMul` 📖	CompOp	—
`instZero` 📖	CompOp	29 math math: `NeBot.nonpos_iff`, `pure_zero`, `NeBot.zero_div_nonneg`, `add_eq_zero_iff`, `NeBot.zero_smul_nonneg`, `map_zero'`, `zero_smul_filter_nonpos`, `NeBot.smul_zero_nonneg`, `not_nonneg_sub_iff`, `tendsto_zero`, `nonpos_iff`, `prod_zero`, `zero_smul_filter`, `coe_pureZeroHom`, `NeBot.zero_mul_nonneg`, `nonneg_sub_iff`, `eventually_zero`, `zero_prod_zero`, `zero_prod`, `nonneg_nhds_iff`, `NeBot.mul_zero_nonneg`, `zero_neBot`, `principal_zero`, `mem_zero`, `NeBot.nonneg_sub`, `map_zero`, `zero_mem_zero`, `pureZeroHom_apply`, `NeBot.div_zero_nonneg`
`mapAddMonoidHom` 📖	CompOp	—
`mapMonoidHom` 📖	CompOp	—
`monoid` 📖	CompOp	4 math math: `isUnit_iff_singleton`, `isUnit_iff`, `isUnit_pure`, `IsUnit.filter`
`mulAction` 📖	CompOp	—
`mulActionFilter` 📖	CompOp	—
`mulDistribMulActionFilter` 📖	CompOp	—
`mulOneClass` 📖	CompOp	2 math math: `pureMonoidHom_apply`, `coe_pureMonoidHom`
`pureAddHom` 📖	CompOp	2 math math: `pureAddHom_apply`, `coe_pureAddHom`
`pureAddMonoidHom` 📖	CompOp	2 math math: `pureAddMonoidHom_apply`, `coe_pureAddMonoidHom`
`pureMonoidHom` 📖	CompOp	2 math math: `pureMonoidHom_apply`, `coe_pureMonoidHom`
`pureMulHom` 📖	CompOp	2 math math: `coe_pureMulHom`, `pureMulHom_apply`
`pureOneHom` 📖	CompOp	2 math math: `pureOneHom_apply`, `coe_pureOneHom`
`pureZeroHom` 📖	CompOp	2 math math: `coe_pureZeroHom`, `pureZeroHom_apply`
`semigroup` 📖	CompOp	—
`subtractionCommMonoid` 📖	CompOp	—
`subtractionMonoid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeftMono` 📖	mathematical	—	`AddLeftMono` `Filter` `instAdd` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`map₂_mono_left`
`addRightMono` 📖	mathematical	—	`AddRightMono` `Filter` `instAdd` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`map₂_mono_right`
`add_bot` 📖	mathematical	—	`Filter` `instAdd` `Bot.bot` `instBot`	—	`map₂_bot_right`
`add_eq_bot_iff` 📖	mathematical	—	`Filter` `instAdd` `Bot.bot` `instBot`	—	`map₂_eq_bot_iff`
`add_eq_zero_iff` 📖	mathematical	—	`Filter` `instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `instPure`	—	`zero_mem_zero` `zero_neBot` `Set.add_eq_zero_iff` `Set.Nonempty.subset_zero_iff` `NeBot.nonempty_of_mem` `add_mem_add` `NeBot.le_pure_iff` `NeBot.of_add_left` `le_pure_iff` `NeBot.of_add_right` `pure_add_pure` `pure_zero`
`add_mem_add` 📖	mathematical	`Set` `Filter` `instMembership`	`instAdd` `Set.add`	—	`image2_mem_map₂`
`add_mul_subset` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instMul` `Distrib.toMul` `instAdd` `Distrib.toAdd`	—	`map₂_distrib_le_right` `add_mul` `Distrib.rightDistribClass`
`add_neBot_iff` 📖	mathematical	—	`NeBot` `Filter` `instAdd`	—	`map₂_neBot_iff`
`add_pure` 📖	mathematical	—	`Filter` `instAdd` `instPure` `map`	—	`map₂_pure_right`
`add_top_of_nonneg` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`instAdd` `AddZero.toAdd` `Top.top` `instTop`	—	`top_le_iff` `mem_add` `mem_top` `Set.univ_subset_iff` `Set.add_univ_of_zero_mem` `mem_zero`
`bot_add` 📖	mathematical	—	`Filter` `instAdd` `Bot.bot` `instBot`	—	`map₂_bot_left`
`bot_div` 📖	mathematical	—	`Filter` `instDiv` `Bot.bot` `instBot`	—	`map₂_bot_left`
`bot_mul` 📖	mathematical	—	`Filter` `instMul` `Bot.bot` `instBot`	—	`map₂_bot_left`
`bot_pow` 📖	mathematical	—	`Filter` `instNPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toMul` `Bot.bot` `instBot`	—	`pow_succ'` `bot_mul`
`bot_smul` 📖	mathematical	—	`Filter` `instSMul` `Bot.bot` `instBot`	—	`map₂_bot_left`
`bot_sub` 📖	mathematical	—	`Filter` `instSub` `Bot.bot` `instBot`	—	`map₂_bot_left`
`bot_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `Filter` `instHVAdd` `instVAdd` `Bot.bot` `instBot`	—	`map₂_bot_left`
`bot_vsub` 📖	mathematical	—	`VSub.vsub` `Filter` `instVSub` `Bot.bot` `instBot`	—	`map₂_bot_left`
`coe_pureAddHom` 📖	mathematical	—	`DFunLike.coe` `AddHom` `Filter` `instAdd` `AddHom.funLike` `pureAddHom` `instPure`	—	—
`coe_pureAddMonoidHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Filter` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoidHom.instFunLike` `pureAddMonoidHom` `instPure`	—	—
`coe_pureMonoidHom` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Filter` `MulOneClass.toMulOne` `mulOneClass` `MonoidHom.instFunLike` `pureMonoidHom` `instPure`	—	—
`coe_pureMulHom` 📖	mathematical	—	`DFunLike.coe` `MulHom` `Filter` `instMul` `MulHom.funLike` `pureMulHom` `instPure`	—	—
`coe_pureOneHom` 📖	mathematical	—	`DFunLike.coe` `OneHom` `Filter` `instOne` `OneHom.funLike` `pureOneHom` `instPure`	—	—
`coe_pureZeroHom` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `Filter` `instZero` `ZeroHom.funLike` `pureZeroHom` `instPure`	—	—
`comap_add_comap_le` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `comap` `DFunLike.coe`	—	`Set.Subset.rfl` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.preimage_add_preimage_subset` `Set.preimage_mono`
`comap_inv` 📖	mathematical	—	`comap` `InvolutiveInv.toInv` `Filter` `instInv`	—	`map_eq_comap_of_inverse` `inv_comp_inv`
`comap_mul_comap_le` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `comap` `DFunLike.coe`	—	`Set.Subset.rfl` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.preimage_mul_preimage_subset` `Set.preimage_mono`
`comap_neg` 📖	mathematical	—	`comap` `InvolutiveNeg.toNeg` `Filter` `instNeg`	—	`map_eq_comap_of_inverse` `neg_comp_neg`
`covariant_div` 📖	mathematical	—	`CovariantClass` `Filter` `instDiv` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`map₂_mono_left`
`covariant_smul` 📖	mathematical	—	`CovariantClass` `Filter` `instSMul` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`map₂_mono_left`
`covariant_smul_filter` 📖	mathematical	—	`CovariantClass` `Filter` `instSMulFilter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`map_mono`
`covariant_sub` 📖	mathematical	—	`CovariantClass` `Filter` `instSub` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`map₂_mono_left`
`covariant_swap_div` 📖	mathematical	—	`CovariantClass` `Filter` `Function.swap` `instDiv` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`map₂_mono_right`
`covariant_swap_sub` 📖	mathematical	—	`CovariantClass` `Filter` `Function.swap` `instSub` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`map₂_mono_right`
`covariant_vadd` 📖	mathematical	—	`CovariantClass` `Filter` `HVAdd.hVAdd` `instHVAdd` `instVAdd` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`map₂_mono_left`
`covariant_vadd_filter` 📖	mathematical	—	`CovariantClass` `Filter` `HVAdd.hVAdd` `instHVAdd` `instVAddFilter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`map_mono`
`div_bot` 📖	mathematical	—	`Filter` `instDiv` `Bot.bot` `instBot`	—	`map₂_bot_right`
`div_eq_bot_iff` 📖	mathematical	—	`Filter` `instDiv` `Bot.bot` `instBot`	—	`map₂_eq_bot_iff`
`div_le_div` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instDiv`	—	`map₂_mono`
`div_le_div_left` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instDiv`	—	`map₂_mono_left`
`div_le_div_right` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instDiv`	—	`map₂_mono_right`
`div_mem_div` 📖	mathematical	`Set` `Filter` `instMembership`	`instDiv` `Set.div`	—	`image2_mem_map₂`
`div_neBot_iff` 📖	mathematical	—	`NeBot` `Filter` `instDiv`	—	`map₂_neBot_iff`
`div_pure` 📖	mathematical	—	`Filter` `instDiv` `instPure` `map`	—	`map₂_pure_right`
`eventually_one` 📖	mathematical	—	`Eventually` `Filter` `instOne`	—	`eventually_pure`
`eventually_zero` 📖	mathematical	—	`Eventually` `Filter` `instZero`	—	`eventually_pure`
`inv_atTop` 📖	mathematical	—	`Filter` `instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `atTop` `PartialOrder.toPreorder` `atBot`	—	`OrderIso.map_atTop` `IsOrderedMonoid.toMulLeftMono` `covariant_swap_mul_of_covariant_mul`
`inv_eq_bot_iff` 📖	mathematical	—	`Filter` `instInv` `Bot.bot` `instBot`	—	`map_eq_bot_iff`
`inv_le_iff_le_inv` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instInv` `InvolutiveInv.toInv`	—	`inv_le_inv_iff` `inv_inv`
`inv_le_inv` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instInv`	—	`map_mono`
`inv_le_inv_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instInv` `InvolutiveInv.toInv`	—	`inv_le_inv` `inv_inv`
`inv_le_self` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instInv` `InvolutiveInv.toInv`	—	`LE.le.antisymm` `inv_le_iff_le_inv` `Eq.le`
`inv_mem_inv` 📖	mathematical	`Set` `Filter` `instMembership`	`instInv` `InvolutiveInv.toInv` `Set.inv`	—	`mem_inv` `Set.inv_preimage` `inv_inv`
`inv_pure` 📖	mathematical	—	`Filter` `instInv` `instPure`	—	—
`isAddUnit_iff` 📖	mathematical	—	`IsAddUnit` `Filter` `addMonoid` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `instPure`	—	`add_eq_zero_iff` `AddUnits.add_neg` `pure_injective` `pure_add_pure` `AddUnits.neg_add` `IsAddUnit.filter`
`isAddUnit_pure` 📖	mathematical	—	`IsAddUnit` `Filter` `addMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instPure`	—	`IsAddUnit.filter` `AddGroup.isAddUnit`
`isCentralScalar` 📖	mathematical	—	`IsCentralScalar` `Filter` `instSMulFilter` `MulOpposite`	—	`IsCentralScalar.op_smul_eq_smul`
`isCentralVAdd` 📖	mathematical	—	`IsCentralVAdd` `Filter` `instVAddFilter` `AddOpposite`	—	`IsCentralVAdd.op_vadd_eq_vadd`
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `Filter` `instSMulFilter`	—	`smul_assoc` `map_map`
`isScalarTower'` 📖	mathematical	—	`IsScalarTower` `Filter` `instSMulFilter` `instSMul`	—	`map_map₂_distrib_left` `smul_assoc`
`isScalarTower''` 📖	mathematical	—	`IsScalarTower` `Filter` `instSMul`	—	`map₂_assoc` `smul_assoc`
`isUnit_iff` 📖	mathematical	—	`IsUnit` `Filter` `monoid` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `instPure`	—	`mul_eq_one_iff` `Units.mul_inv` `pure_injective` `pure_mul_pure` `Units.inv_mul` `IsUnit.filter`
`isUnit_iff_singleton` 📖	mathematical	—	`IsUnit` `Filter` `monoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instPure`	—	—
`isUnit_pure` 📖	mathematical	—	`IsUnit` `Filter` `monoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instPure`	—	`IsUnit.filter` `Group.isUnit`
`le_add_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instAdd` `Set` `instMembership` `Set.add`	—	`le_map₂_iff`
`le_div_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instDiv` `Set` `instMembership` `Set.div`	—	`le_map₂_iff`
`le_mul_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instMul` `Set` `instMembership` `Set.mul`	—	`le_map₂_iff`
`le_one_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOne` `Set` `instMembership` `Set.one`	—	`le_pure_iff`
`le_smul_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instSMul` `Set` `instMembership` `Set.smul`	—	`le_map₂_iff`
`le_sub_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instSub` `Set` `instMembership` `Set.sub`	—	`le_map₂_iff`
`le_vadd_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `HVAdd.hVAdd` `instHVAdd` `instVAdd` `Set` `instMembership` `Set.vadd`	—	`le_map₂_iff`
`le_vsub_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `VSub.vsub` `instVSub` `Set` `instMembership` `Set.vsub`	—	`le_map₂_iff`
`map_add` 📖	mathematical	—	`map` `DFunLike.coe` `Filter` `instAdd`	—	`map_map₂_distrib` `map_add`
`map_div` 📖	mathematical	—	`map` `DFunLike.coe` `Filter` `instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `DivisionMonoid.toDivInvMonoid`	—	`map_map₂_distrib` `map_div`
`map_inv` 📖	mathematical	—	`map` `Filter` `instInv`	—	—
`map_inv'` 📖	mathematical	—	`map` `DFunLike.coe` `Filter` `instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Function.Semiconj.filter_map` `map_inv`
`map_mul` 📖	mathematical	—	`map` `DFunLike.coe` `Filter` `instMul`	—	`map_map₂_distrib` `map_mul`
`map_neg` 📖	mathematical	—	`map` `Filter` `instNeg`	—	—
`map_neg'` 📖	mathematical	—	`map` `DFunLike.coe` `Filter` `instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Function.Semiconj.filter_map` `map_neg`
`map_one` 📖	mathematical	—	`map` `DFunLike.coe` `Filter` `instOne`	—	`map_one`
`map_one'` 📖	mathematical	—	`map` `Filter` `instOne` `instPure`	—	—
`map_smul` 📖	mathematical	—	`map` `Filter` `instSMulFilter`	—	—
`map_sub` 📖	mathematical	—	`map` `DFunLike.coe` `Filter` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SubtractionMonoid.toSubNegMonoid`	—	`map_map₂_distrib` `map_sub`
`map_vadd` 📖	mathematical	—	`map` `HVAdd.hVAdd` `instHVAdd` `Filter` `instVAddFilter`	—	—
`map_zero` 📖	mathematical	—	`map` `DFunLike.coe` `Filter` `instZero`	—	`map_zero`
`map_zero'` 📖	mathematical	—	`map` `Filter` `instZero` `instPure`	—	—
`map₂_add` 📖	mathematical	—	`map₂` `Filter` `instAdd`	—	—
`map₂_div` 📖	mathematical	—	`map₂` `Filter` `instDiv`	—	—
`map₂_mul` 📖	mathematical	—	`map₂` `Filter` `instMul`	—	—
`map₂_smul` 📖	mathematical	—	`map₂` `Filter` `instSMul`	—	—
`map₂_sub` 📖	mathematical	—	`map₂` `Filter` `instSub`	—	—
`map₂_vadd` 📖	mathematical	—	`map₂` `HVAdd.hVAdd` `instHVAdd` `Filter` `instVAdd`	—	—
`map₂_vsub` 📖	mathematical	—	`map₂` `VSub.vsub` `Filter` `instVSub`	—	—
`mem_add` 📖	mathematical	—	`Set` `Filter` `instMembership` `instAdd` `Set.instHasSubset` `Set.add`	—	—
`mem_div` 📖	mathematical	—	`Set` `Filter` `instMembership` `instDiv` `Set.instHasSubset` `Set.div`	—	—
`mem_inv` 📖	mathematical	—	`Set` `Filter` `instMembership` `instInv` `Set.preimage`	—	—
`mem_mul` 📖	mathematical	—	`Set` `Filter` `instMembership` `instMul` `Set.instHasSubset` `Set.mul`	—	—
`mem_neg` 📖	mathematical	—	`Set` `Filter` `instMembership` `instNeg` `Set.preimage`	—	—
`mem_one` 📖	mathematical	—	`Set` `Filter` `instMembership` `instOne` `Set.instMembership`	—	`mem_pure`
`mem_smul` 📖	mathematical	—	`Set` `Filter` `instMembership` `instSMul` `Set.instHasSubset` `Set.smul`	—	—
`mem_smul_filter` 📖	mathematical	—	`Set` `Filter` `instMembership` `instSMulFilter` `Set.preimage`	—	—
`mem_sub` 📖	mathematical	—	`Set` `Filter` `instMembership` `instSub` `Set.instHasSubset` `Set.sub`	—	—
`mem_vadd` 📖	mathematical	—	`Set` `Filter` `instMembership` `HVAdd.hVAdd` `instHVAdd` `instVAdd` `Set.instHasSubset` `Set.vadd`	—	—
`mem_vadd_filter` 📖	mathematical	—	`Set` `Filter` `instMembership` `HVAdd.hVAdd` `instHVAdd` `instVAddFilter` `Set.preimage`	—	—
`mem_vsub` 📖	mathematical	—	`Set` `Filter` `instMembership` `VSub.vsub` `instVSub` `Set.instHasSubset` `Set.vsub`	—	—
`mem_zero` 📖	mathematical	—	`Set` `Filter` `instMembership` `instZero` `Set.instMembership`	—	`mem_pure`
`mulLeftMono` 📖	mathematical	—	`MulLeftMono` `Filter` `instMul` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`map₂_mono_left`
`mulRightMono` 📖	mathematical	—	`MulRightMono` `Filter` `instMul` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`map₂_mono_right`
`mul_add_subset` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instMul` `Distrib.toMul` `instAdd` `Distrib.toAdd`	—	`map₂_distrib_le_left` `mul_add` `Distrib.leftDistribClass`
`mul_bot` 📖	mathematical	—	`Filter` `instMul` `Bot.bot` `instBot`	—	`map₂_bot_right`
`mul_eq_bot_iff` 📖	mathematical	—	`Filter` `instMul` `Bot.bot` `instBot`	—	`map₂_eq_bot_iff`
`mul_eq_one_iff` 📖	mathematical	—	`Filter` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `instOne` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `instPure`	—	`one_mem_one` `one_neBot` `Set.mul_eq_one_iff` `Set.Nonempty.subset_one_iff` `NeBot.nonempty_of_mem` `mul_mem_mul` `NeBot.le_pure_iff` `NeBot.of_mul_left` `le_pure_iff` `NeBot.of_mul_right` `pure_mul_pure` `pure_one`
`mul_mem_mul` 📖	mathematical	`Set` `Filter` `instMembership`	`instMul` `Set.mul`	—	`image2_mem_map₂`
`mul_neBot_iff` 📖	mathematical	—	`NeBot` `Filter` `instMul`	—	`map₂_neBot_iff`
`mul_pure` 📖	mathematical	—	`Filter` `instMul` `instPure` `map`	—	`map₂_pure_right`
`mul_top_of_one_le` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`instMul` `MulOne.toMul` `Top.top` `instTop`	—	`top_le_iff` `Set.univ_subset_iff` `Set.mul_univ_of_one_mem` `mem_one`
`neBot_inv_iff` 📖	mathematical	—	`NeBot` `Filter` `instInv`	—	`map_neBot_iff`
`neBot_neg_iff` 📖	mathematical	—	`NeBot` `Filter` `instNeg`	—	`map_neBot_iff`
`neg_atTop` 📖	mathematical	—	`Filter` `instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `atTop` `PartialOrder.toPreorder` `atBot`	—	`OrderIso.map_atTop` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`neg_eq_bot_iff` 📖	mathematical	—	`Filter` `instNeg` `Bot.bot` `instBot`	—	`map_eq_bot_iff`
`neg_le_iff_le_neg` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instNeg` `InvolutiveNeg.toNeg`	—	`neg_le_neg_iff` `neg_neg`
`neg_le_neg` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instNeg`	—	`map_mono`
`neg_le_neg_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instNeg` `InvolutiveNeg.toNeg`	—	`neg_le_neg` `neg_neg`
`neg_le_self` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instNeg` `InvolutiveNeg.toNeg`	—	`LE.le.antisymm` `neg_le_iff_le_neg` `Eq.le`
`neg_mem_neg` 📖	mathematical	`Set` `Filter` `instMembership`	`instNeg` `InvolutiveNeg.toNeg` `Set.neg`	—	`mem_neg` `Set.neg_preimage` `neg_neg`
`neg_pure` 📖	mathematical	—	`Filter` `instNeg` `instPure`	—	—
`nonneg_sub_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Disjoint` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `instCompleteLatticeFilter`	—	`Disjoint.le_bot` `mem_bot` `Set.zero_mem_sub_iff` `sub_mem_sub` `disjoint_iff` `disjoint_of_disjoint_of_mem`
`nonpos_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instZero` `Set` `instMembership` `Set.zero`	—	`le_pure_iff`
`not_nonneg_sub_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Disjoint` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `instCompleteLatticeFilter`	—	`Iff.not_left` `nonneg_sub_iff`
`not_one_le_div_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOne` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `Disjoint` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `instCompleteLatticeFilter`	—	`Iff.not_left` `one_le_div_iff`
`nsmul_bot` 📖	mathematical	—	`Filter` `instNSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toAdd` `Bot.bot` `instBot`	—	`succ_nsmul'` `bot_add`
`nsmul_mem_nsmul` 📖	mathematical	`Set` `Filter` `instMembership`	`instNSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toAdd` `Set.NSMul`	—	`zero_nsmul` `zero_mem_zero` `succ_nsmul` `add_mem_add`
`nsmul_top` 📖	mathematical	—	`Filter` `instNSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toAdd` `Top.top` `instTop`	—	`one_nsmul` `succ_nsmul` `top_add_top`
`one_le_div_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOne` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `Disjoint` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `instCompleteLatticeFilter`	—	`Disjoint.le_bot` `mem_bot` `Set.one_mem_div_iff` `div_mem_div` `disjoint_iff` `disjoint_of_disjoint_of_mem`
`one_mem_one` 📖	mathematical	—	`Set` `Filter` `instMembership` `instOne` `Set.one`	—	`mem_pure` `Set.one_mem_one`
`one_neBot` 📖	mathematical	—	`NeBot` `Filter` `instOne`	—	`pure_neBot`
`one_prod` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `instOne` `map`	—	`pure_prod`
`one_prod_one` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `instOne` `Prod.instOne`	—	`prod_pure_pure`
`pow_mem_pow` 📖	mathematical	`Set` `Filter` `instMembership`	`instNPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toMul` `Set.NPow`	—	`pow_zero` `one_mem_one` `pow_succ` `mul_mem_mul`
`principal_one` 📖	mathematical	—	`principal` `Set` `Set.one` `Filter` `instOne`	—	`principal_singleton`
`principal_zero` 📖	mathematical	—	`principal` `Set` `Set.zero` `Filter` `instZero`	—	`principal_singleton`
`prod_one` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `instOne` `map`	—	`prod_pure`
`prod_zero` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `instZero` `map`	—	`prod_pure`
`pureAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `Filter` `instAdd` `AddHom.funLike` `pureAddHom` `instPure`	—	—
`pureAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Filter` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoidHom.instFunLike` `pureAddMonoidHom` `instPure`	—	—
`pureMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Filter` `MulOneClass.toMulOne` `mulOneClass` `MonoidHom.instFunLike` `pureMonoidHom` `instPure`	—	—
`pureMulHom_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `Filter` `instMul` `MulHom.funLike` `pureMulHom` `instPure`	—	—
`pureOneHom_apply` 📖	mathematical	—	`DFunLike.coe` `OneHom` `Filter` `instOne` `OneHom.funLike` `pureOneHom` `instPure`	—	—
`pureZeroHom_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `Filter` `instZero` `ZeroHom.funLike` `pureZeroHom` `instPure`	—	—
`pure_add` 📖	mathematical	—	`Filter` `instAdd` `instPure` `map`	—	`map₂_pure_left`
`pure_add_pure` 📖	mathematical	—	`Filter` `instAdd` `instPure`	—	`add_pure`
`pure_div` 📖	mathematical	—	`Filter` `instDiv` `instPure` `map`	—	`map₂_pure_left`
`pure_div_pure` 📖	mathematical	—	`Filter` `instDiv` `instPure`	—	`div_pure`
`pure_mul` 📖	mathematical	—	`Filter` `instMul` `instPure` `map`	—	`map₂_pure_left`
`pure_mul_pure` 📖	mathematical	—	`Filter` `instMul` `instPure`	—	`mul_pure`
`pure_one` 📖	mathematical	—	`Filter` `instPure` `instOne`	—	—
`pure_smul` 📖	mathematical	—	`Filter` `instSMul` `instPure` `map`	—	`map₂_pure_left`
`pure_smul_pure` 📖	mathematical	—	`Filter` `instSMul` `instPure`	—	`smul_pure`
`pure_sub` 📖	mathematical	—	`Filter` `instSub` `instPure` `map`	—	`map₂_pure_left`
`pure_sub_pure` 📖	mathematical	—	`Filter` `instSub` `instPure`	—	`sub_pure`
`pure_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `Filter` `instHVAdd` `instVAdd` `instPure` `map`	—	`map₂_pure_left`
`pure_vadd_pure` 📖	mathematical	—	`HVAdd.hVAdd` `Filter` `instHVAdd` `instVAdd` `instPure`	—	`vadd_pure`
`pure_vsub` 📖	mathematical	—	`VSub.vsub` `Filter` `instVSub` `instPure` `map`	—	`map₂_pure_left`
`pure_vsub_pure` 📖	mathematical	—	`VSub.vsub` `Filter` `instVSub` `instPure`	—	`vsub_pure`
`pure_zero` 📖	mathematical	—	`Filter` `instPure` `instZero`	—	—
`smulCommClass` 📖	mathematical	—	`SMulCommClass` `Filter` `instSMul`	—	`map₂_left_comm` `SMulCommClass.smul_comm`
`smulCommClass_filter` 📖	mathematical	—	`SMulCommClass` `Filter` `instSMulFilter`	—	`map_comm` `SMulCommClass.smul_comm`
`smulCommClass_filter'` 📖	mathematical	—	`SMulCommClass` `Filter` `instSMulFilter` `instSMul`	—	`map_map₂_distrib_right` `SMulCommClass.smul_comm`
`smulCommClass_filter''` 📖	mathematical	—	`SMulCommClass` `Filter` `instSMul` `instSMulFilter`	—	`SMulCommClass.symm` `smulCommClass_filter'`
`smul_bot` 📖	mathematical	—	`Filter` `instSMul` `Bot.bot` `instBot`	—	`map₂_bot_right`
`smul_eq_bot_iff` 📖	mathematical	—	`Filter` `instSMul` `Bot.bot` `instBot`	—	`map₂_eq_bot_iff`
`smul_filter_bot` 📖	mathematical	—	`Filter` `instSMulFilter` `Bot.bot` `instBot`	—	`map_bot`
`smul_filter_eq_bot_iff` 📖	mathematical	—	`Filter` `instSMulFilter` `Bot.bot` `instBot`	—	`map_eq_bot_iff`
`smul_filter_le_smul_filter` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instSMulFilter`	—	`map_mono`
`smul_filter_neBot_iff` 📖	mathematical	—	`NeBot` `Filter` `instSMulFilter`	—	`map_neBot_iff`
`smul_le_smul` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instSMul`	—	`map₂_mono`
`smul_le_smul_left` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instSMul`	—	`map₂_mono_left`
`smul_le_smul_right` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instSMul`	—	`map₂_mono_right`
`smul_mem_smul` 📖	mathematical	`Set` `Filter` `instMembership`	`instSMul` `Set.smul`	—	`image2_mem_map₂`
`smul_neBot_iff` 📖	mathematical	—	`NeBot` `Filter` `instSMul`	—	`map₂_neBot_iff`
`smul_pure` 📖	mathematical	—	`Filter` `instSMul` `instPure` `map`	—	`map₂_pure_right`
`smul_set_mem_smul_filter` 📖	mathematical	`Set` `Filter` `instMembership`	`instSMulFilter` `Set.smulSet`	—	`image_mem_map`
`smul_tendsto_smul_iff` 📖	mathematical	—	`Tendsto` `Pi.instSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Filter` `instSMulFilter`	—	`IsUnit.smul_tendsto_smul_iff` `Group.isUnit`
`smul_tendsto_smul_iff₀` 📖	mathematical	—	`Tendsto` `Pi.instSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `Filter` `instSMulFilter`	—	`IsUnit.smul_tendsto_smul_iff` `Ne.isUnit`
`sub_bot` 📖	mathematical	—	`Filter` `instSub` `Bot.bot` `instBot`	—	`map₂_bot_right`
`sub_eq_bot_iff` 📖	mathematical	—	`Filter` `instSub` `Bot.bot` `instBot`	—	`map₂_eq_bot_iff`
`sub_le_sub` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instSub`	—	`map₂_mono`
`sub_le_sub_left` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instSub`	—	`map₂_mono_left`
`sub_le_sub_right` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instSub`	—	`map₂_mono_right`
`sub_mem_sub` 📖	mathematical	`Set` `Filter` `instMembership`	`instSub` `Set.sub`	—	`image2_mem_map₂`
`sub_neBot_iff` 📖	mathematical	—	`NeBot` `Filter` `instSub`	—	`map₂_neBot_iff`
`sub_pure` 📖	mathematical	—	`Filter` `instSub` `instPure` `map`	—	`map₂_pure_right`
`tendsto_one` 📖	mathematical	—	`Tendsto` `Filter` `instOne` `Eventually`	—	`tendsto_pure`
`tendsto_zero` 📖	mathematical	—	`Tendsto` `Filter` `instZero` `Eventually`	—	`tendsto_pure`
`top_add_of_nonneg` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`instAdd` `AddZero.toAdd` `Top.top` `instTop`	—	`top_le_iff` `mem_add` `mem_top` `Set.univ_subset_iff` `Set.univ_add_of_zero_mem` `mem_zero`
`top_add_top` 📖	mathematical	—	`Filter` `instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Top.top` `instTop`	—	`add_top_of_nonneg` `le_top`
`top_mul_of_one_le` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`instMul` `MulOne.toMul` `Top.top` `instTop`	—	`top_le_iff` `Set.univ_subset_iff` `Set.univ_mul_of_one_mem` `mem_one`
`top_mul_top` 📖	mathematical	—	`Filter` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Top.top` `instTop`	—	`mul_top_of_one_le` `le_top`
`top_pow` 📖	mathematical	—	`Filter` `instNPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toMul` `Top.top` `instTop`	—	`pow_one` `pow_succ` `top_mul_top`
`vaddAssocClass` 📖	mathematical	—	`VAddAssocClass` `Filter` `instVAddFilter`	—	`vadd_assoc` `map_map`
`vaddAssocClass'` 📖	mathematical	—	`VAddAssocClass` `Filter` `instVAddFilter` `instVAdd`	—	`map_map₂_distrib_left` `vadd_assoc`
`vaddAssocClass''` 📖	mathematical	—	`VAddAssocClass` `Filter` `instVAdd`	—	`map₂_assoc` `vadd_assoc`
`vaddCommClass` 📖	mathematical	—	`VAddCommClass` `Filter` `instVAdd`	—	`map₂_left_comm` `VAddCommClass.vadd_comm`
`vaddCommClass_filter` 📖	mathematical	—	`VAddCommClass` `Filter` `instVAddFilter`	—	`map_comm` `VAddCommClass.vadd_comm`
`vaddCommClass_filter'` 📖	mathematical	—	`VAddCommClass` `Filter` `instVAddFilter` `instVAdd`	—	`map_map₂_distrib_right` `VAddCommClass.vadd_comm`
`vaddCommClass_filter''` 📖	mathematical	—	`VAddCommClass` `Filter` `instVAdd` `instVAddFilter`	—	`VAddCommClass.symm` `vaddCommClass_filter'`
`vadd_bot` 📖	mathematical	—	`HVAdd.hVAdd` `Filter` `instHVAdd` `instVAdd` `Bot.bot` `instBot`	—	`map₂_bot_right`
`vadd_eq_bot_iff` 📖	mathematical	—	`HVAdd.hVAdd` `Filter` `instHVAdd` `instVAdd` `Bot.bot` `instBot`	—	`map₂_eq_bot_iff`
`vadd_filter_bot` 📖	mathematical	—	`HVAdd.hVAdd` `Filter` `instHVAdd` `instVAddFilter` `Bot.bot` `instBot`	—	`map_bot`
`vadd_filter_eq_bot_iff` 📖	mathematical	—	`HVAdd.hVAdd` `Filter` `instHVAdd` `instVAddFilter` `Bot.bot` `instBot`	—	`map_eq_bot_iff`
`vadd_filter_le_vadd_filter` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`HVAdd.hVAdd` `instHVAdd` `instVAddFilter`	—	`map_mono`
`vadd_filter_neBot_iff` 📖	mathematical	—	`NeBot` `HVAdd.hVAdd` `Filter` `instHVAdd` `instVAddFilter`	—	`map_neBot_iff`
`vadd_le_vadd` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`HVAdd.hVAdd` `instHVAdd` `instVAdd`	—	`map₂_mono`
`vadd_le_vadd_left` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`HVAdd.hVAdd` `instHVAdd` `instVAdd`	—	`map₂_mono_left`
`vadd_le_vadd_right` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`HVAdd.hVAdd` `instHVAdd` `instVAdd`	—	`map₂_mono_right`
`vadd_mem_vadd` 📖	mathematical	`Set` `Filter` `instMembership`	`HVAdd.hVAdd` `instHVAdd` `instVAdd` `Set.vadd`	—	`image2_mem_map₂`
`vadd_neBot_iff` 📖	mathematical	—	`NeBot` `HVAdd.hVAdd` `Filter` `instHVAdd` `instVAdd`	—	`map₂_neBot_iff`
`vadd_pure` 📖	mathematical	—	`HVAdd.hVAdd` `Filter` `instHVAdd` `instVAdd` `instPure` `map`	—	`map₂_pure_right`
`vadd_set_mem_vadd_filter` 📖	mathematical	`Set` `Filter` `instMembership`	`HVAdd.hVAdd` `instHVAdd` `instVAddFilter` `Set.vaddSet`	—	`image_mem_map`
`vadd_tendsto_vadd_iff` 📖	mathematical	—	`Tendsto` `HVAdd.hVAdd` `instHVAdd` `Pi.instVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Filter` `instVAddFilter`	—	`IsAddUnit.vadd_tendsto_vadd_iff` `AddGroup.isAddUnit`
`vsub_bot` 📖	mathematical	—	`VSub.vsub` `Filter` `instVSub` `Bot.bot` `instBot`	—	`map₂_bot_right`
`vsub_eq_bot_iff` 📖	mathematical	—	`VSub.vsub` `Filter` `instVSub` `Bot.bot` `instBot`	—	`map₂_eq_bot_iff`
`vsub_le_vsub` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`VSub.vsub` `instVSub`	—	`map₂_mono`
`vsub_le_vsub_left` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`VSub.vsub` `instVSub`	—	`map₂_mono_left`
`vsub_le_vsub_right` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`VSub.vsub` `instVSub`	—	`map₂_mono_right`
`vsub_mem_vsub` 📖	mathematical	`Set` `Filter` `instMembership`	`VSub.vsub` `instVSub` `Set.vsub`	—	`image2_mem_map₂`
`vsub_neBot_iff` 📖	mathematical	—	`NeBot` `VSub.vsub` `Filter` `instVSub`	—	`map₂_neBot_iff`
`vsub_pure` 📖	mathematical	—	`VSub.vsub` `Filter` `instVSub` `instPure` `map`	—	`map₂_pure_right`
`zero_mem_zero` 📖	mathematical	—	`Set` `Filter` `instMembership` `instZero` `Set.zero`	—	`mem_pure` `Set.zero_mem_zero`
`zero_neBot` 📖	mathematical	—	`NeBot` `Filter` `instZero`	—	`pure_neBot`
`zero_prod` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `instZero` `map`	—	`pure_prod`
`zero_prod_zero` 📖	mathematical	—	`SProd.sprod` `Filter` `instSProd` `instZero` `Prod.instZero`	—	`prod_pure_pure`
`zero_smul_filter` 📖	mathematical	—	`Filter` `instSMulFilter` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `instZero`	—	`LE.le.antisymm` `zero_smul_filter_nonpos` `le_map_iff` `Set.image_congr` `zero_smul` `Set.Nonempty.image_const` `NeBot.nonempty_of_mem` `zero_mem_zero`
`zero_smul_filter_nonpos` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instSMulFilter` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `instZero`	—	`mem_smul_filter` `Set.eq_univ_iff_forall` `Set.mem_preimage` `zero_smul` `univ_mem`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Filter.HasBasis`	`Filter` `Filter.instAdd` `Set` `Set.add`	—	`map₂`
`div` 📖	mathematical	`Filter.HasBasis`	`Filter` `Filter.instDiv` `Set` `Set.div`	—	`map₂`
`inv` 📖	mathematical	`Filter.HasBasis`	`Filter` `Filter.instInv` `InvolutiveInv.toInv` `Set` `Set.inv`	—	`Set.image_inv_eq_inv` `map`
`mul` 📖	mathematical	`Filter.HasBasis`	`Filter` `Filter.instMul` `Set` `Set.mul`	—	`map₂`
`neg` 📖	mathematical	`Filter.HasBasis`	`Filter` `Filter.instNeg` `InvolutiveNeg.toNeg` `Set` `Set.neg`	—	`Set.image_neg_eq_neg` `map`
`smul` 📖	mathematical	`Filter.HasBasis`	`Filter` `Filter.instSMul` `Set` `Set.smul`	—	`map₂`
`sub` 📖	mathematical	`Filter.HasBasis`	`Filter` `Filter.instSub` `Set` `Set.sub`	—	`map₂`
`vadd` 📖	mathematical	`Filter.HasBasis`	`HVAdd.hVAdd` `Filter` `instHVAdd` `Filter.instVAdd` `Set` `Set.vadd`	—	`map₂`

Filter.NeBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instAdd`	—	`map₂`
`div` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instDiv`	—	`map₂`
`div_zero_nonneg` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instZero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `Filter.instDiv` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`Filter.le_div_iff` `nonempty_of_mem` `div_zero`
`inv` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instInv`	—	`map`
`le_one_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instOne`	—	`le_pure_iff`
`mul` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instMul`	—	`map₂`
`mul_zero_nonneg` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instZero` `MulZeroClass.toZero` `Filter.instMul` `MulZeroClass.toMul`	—	`Filter.le_mul_iff` `nonempty_of_mem` `MulZeroClass.mul_zero`
`neg` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instNeg`	—	`map`
`nonneg_sub` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Filter.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`Filter.nonneg_sub_iff` `disjoint_self` `Filter.neBot_iff`
`nonpos_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instZero`	—	`le_pure_iff`
`of_add_left` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_left`
`of_add_right` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_right`
`of_div_left` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_left`
`of_div_right` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_right`
`of_mul_left` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_left`
`of_mul_right` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_right`
`of_smul_filter` 📖	mathematical	—	`Filter.NeBot`	—	`of_map`
`of_smul_left` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_left`
`of_smul_right` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_right`
`of_sub_left` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_left`
`of_sub_right` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_right`
`of_vadd_filter` 📖	mathematical	—	`Filter.NeBot`	—	`of_map`
`of_vadd_left` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_left`
`of_vadd_right` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_right`
`of_vsub_left` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_left`
`of_vsub_right` 📖	mathematical	—	`Filter.NeBot`	—	`of_map₂_right`
`one_le_div` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instOne` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Filter.instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`Filter.neBot_iff`
`smul` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instSMul`	—	`map₂`
`smul_filter` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instSMulFilter`	—	`map`
`smul_zero_nonneg` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instZero` `Filter.instSMul` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`Filter.le_smul_iff` `nonempty_of_mem` `smul_zero`
`sub` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instSub`	—	`map₂`
`vadd` 📖	mathematical	—	`Filter.NeBot` `HVAdd.hVAdd` `Filter` `instHVAdd` `Filter.instVAdd`	—	`map₂`
`vadd_filter` 📖	mathematical	—	`Filter.NeBot` `HVAdd.hVAdd` `Filter` `instHVAdd` `Filter.instVAddFilter`	—	`map`
`vsub` 📖	mathematical	—	`Filter.NeBot` `VSub.vsub` `Filter` `Filter.instVSub`	—	`map₂`
`zero_div_nonneg` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instZero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `Filter.instDiv` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`Filter.le_div_iff` `nonempty_of_mem` `zero_div`
`zero_mul_nonneg` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instZero` `MulZeroClass.toZero` `Filter.instMul` `MulZeroClass.toMul`	—	`Filter.le_mul_iff` `nonempty_of_mem` `MulZeroClass.zero_mul`
`zero_smul_nonneg` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instZero` `Filter.instSMul` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`Filter.le_smul_iff` `nonempty_of_mem` `zero_smul`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_add` 📖	mathematical	`Filter.Tendsto` `DFunLike.coe`	`Filter` `Filter.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`Eq.trans_le` `Filter.map_add` `add_le_add` `Filter.addLeftMono` `Filter.addRightMono`
`div_div` 📖	mathematical	`Filter.Tendsto` `DFunLike.coe`	`Filter` `Filter.instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `DivisionMonoid.toDivInvMonoid`	—	`Eq.trans_le` `Filter.map_div` `Filter.div_le_div`
`inv_inv` 📖	mathematical	`Filter.Tendsto` `DFunLike.coe`	`Filter` `Filter.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Eq.trans_le` `Filter.map_inv'` `Filter.inv_le_inv`
`mul_mul` 📖	mathematical	`Filter.Tendsto` `DFunLike.coe`	`Filter` `Filter.instMul` `MulOne.toMul` `MulOneClass.toMulOne`	—	`Eq.trans_le` `Filter.map_mul` `mul_le_mul'` `Filter.mulLeftMono` `Filter.mulRightMono`
`neg_neg` 📖	mathematical	`Filter.Tendsto` `DFunLike.coe`	`Filter` `Filter.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Eq.trans_le` `Filter.map_neg'` `Filter.neg_le_neg`
`sub_sub` 📖	mathematical	`Filter.Tendsto` `DFunLike.coe`	`Filter` `Filter.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SubtractionMonoid.toSubNegMonoid`	—	`Eq.trans_le` `Filter.map_sub` `Filter.sub_le_sub`

Filter.add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNeBot` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instAdd`	—	`Filter.NeBot.add`

Filter.div

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNeBot` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instDiv`	—	`Filter.NeBot.div`

Filter.inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNeBot` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instInv`	—	`Filter.NeBot.inv`

Filter.mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNeBot` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instMul`	—	`Filter.NeBot.mul`

Filter.neg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNeBot` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instNeg`	—	`Filter.NeBot.neg`

Filter.smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNeBot` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instSMul`	—	`Filter.NeBot.smul`

Filter.smul_filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNeBot` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instSMulFilter`	—	`Filter.NeBot.smul_filter`

Filter.sub

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNeBot` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instSub`	—	`Filter.NeBot.sub`

Filter.vadd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNeBot` 📖	mathematical	—	`Filter.NeBot` `HVAdd.hVAdd` `Filter` `instHVAdd` `Filter.instVAdd`	—	`Filter.NeBot.vadd`

Filter.vadd_filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNeBot` 📖	mathematical	—	`Filter.NeBot` `HVAdd.hVAdd` `Filter` `instHVAdd` `Filter.instVAddFilter`	—	`Filter.NeBot.vadd_filter`

Filter.vsub

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNeBot` 📖	mathematical	—	`Filter.NeBot` `VSub.vsub` `Filter` `Filter.instVSub`	—	`Filter.NeBot.vsub`

IsAddUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`filter` 📖	mathematical	`IsAddUnit`	`Filter` `Filter.addMonoid` `Filter.instPure`	—	`map` `AddMonoidHom.instAddMonoidHomClass`
`vadd_tendsto_vadd_iff` 📖	mathematical	`IsAddUnit`	`Filter.Tendsto` `HVAdd.hVAdd` `instHVAdd` `Pi.instVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `Filter` `Filter.instVAddFilter`	—	`exists_neg'` `vadd_vadd` `zero_vadd` `Filter.Tendsto.comp` `Filter.tendsto_map`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`filter` 📖	mathematical	`IsUnit`	`Filter` `Filter.monoid` `Filter.instPure`	—	`map` `MonoidHom.instMonoidHomClass`
`smul_tendsto_smul_iff` 📖	mathematical	`IsUnit`	`Filter.Tendsto` `Pi.instSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Filter` `Filter.instSMulFilter`	—	`exists_left_inv` `smul_smul` `one_smul` `Filter.Tendsto.comp` `Filter.tendsto_map`

---

← Back to Index