Documentation

Mathlib.Order.Filter.Pointwise

Pointwise operations on filters #

This file defines pointwise operations on filters. This is useful because usual algebraic operations distribute over pointwise operations. For example,

Main declarations #

For α a semigroup/monoid, Filter α is a semigroup/monoid. As an unfortunate side effect, this means that n • f, where n : ℕ, is ambiguous between pointwise scaling and repeated pointwise addition. See note [pointwise nat action].

Implementation notes #

We put all instances in the locale Pointwise, so that these instances are not available by default. Note that we do not mark them as reducible (as argued by note [reducible non-instances]) since we expect the locale to be open whenever the instances are actually used (and making the instances reducible changes the behavior of simp).

Tags #

filter multiplication, filter addition, pointwise addition, pointwise multiplication,

0/1 as filters #

def Filter.instZero {α : Type u_2} [Zero α] :

0 : Filter α is defined as the filter of sets containing 0 : α in locale Pointwise.

Equations
  • Filter.instZero = { zero := pure 0 }
Instances For
    def Filter.instOne {α : Type u_2} [One α] :
    One (Filter α)

    1 : Filter α is defined as the filter of sets containing 1 : α in locale Pointwise.

    Equations
    • Filter.instOne = { one := pure 1 }
    Instances For
      @[simp]
      theorem Filter.mem_zero {α : Type u_2} [Zero α] {s : Set α} :
      s 0 0 s
      @[simp]
      theorem Filter.mem_one {α : Type u_2} [One α] {s : Set α} :
      s 1 1 s
      theorem Filter.zero_mem_zero {α : Type u_2} [Zero α] :
      0 0
      theorem Filter.one_mem_one {α : Type u_2} [One α] :
      1 1
      @[simp]
      theorem Filter.pure_zero {α : Type u_2} [Zero α] :
      pure 0 = 0
      @[simp]
      theorem Filter.pure_one {α : Type u_2} [One α] :
      pure 1 = 1
      @[simp]
      theorem Filter.principal_zero {α : Type u_2} [Zero α] :
      @[simp]
      theorem Filter.principal_one {α : Type u_2} [One α] :
      theorem Filter.zero_neBot {α : Type u_2} [Zero α] :
      theorem Filter.one_neBot {α : Type u_2} [One α] :
      @[simp]
      theorem Filter.map_zero' {α : Type u_2} {β : Type u_3} [Zero α] (f : αβ) :
      Filter.map f 0 = pure (f 0)
      @[simp]
      theorem Filter.map_one' {α : Type u_2} {β : Type u_3} [One α] (f : αβ) :
      Filter.map f 1 = pure (f 1)
      @[simp]
      theorem Filter.nonpos_iff {α : Type u_2} [Zero α] {f : Filter α} :
      f 0 0 f
      @[simp]
      theorem Filter.le_one_iff {α : Type u_2} [One α] {f : Filter α} :
      f 1 1 f
      theorem Filter.NeBot.nonpos_iff {α : Type u_2} [Zero α] {f : Filter α} (h : Filter.NeBot f) :
      f 0 f = 0
      theorem Filter.NeBot.le_one_iff {α : Type u_2} [One α] {f : Filter α} (h : Filter.NeBot f) :
      f 1 f = 1
      @[simp]
      theorem Filter.eventually_zero {α : Type u_2} [Zero α] {p : αProp} :
      (∀ᶠ (x : α) in 0, p x) p 0
      @[simp]
      theorem Filter.eventually_one {α : Type u_2} [One α] {p : αProp} :
      (∀ᶠ (x : α) in 1, p x) p 1
      @[simp]
      theorem Filter.tendsto_zero {α : Type u_2} {β : Type u_3} [Zero α] {a : Filter β} {f : βα} :
      Filter.Tendsto f a 0 ∀ᶠ (x : β) in a, f x = 0
      @[simp]
      theorem Filter.tendsto_one {α : Type u_2} {β : Type u_3} [One α] {a : Filter β} {f : βα} :
      Filter.Tendsto f a 1 ∀ᶠ (x : β) in a, f x = 1
      @[simp]
      theorem Filter.zero_sum_zero {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] :
      0 ×ˢ 0 = 0
      @[simp]
      theorem Filter.one_prod_one {α : Type u_2} {β : Type u_3} [One α] [One β] :
      1 ×ˢ 1 = 1
      def Filter.pureZeroHom {α : Type u_2} [Zero α] :
      ZeroHom α (Filter α)

      pure as a ZeroHom.

      Equations
      • Filter.pureZeroHom = { toFun := pure, map_zero' := (_ : pure 0 = 0) }
      Instances For
        def Filter.pureOneHom {α : Type u_2} [One α] :
        OneHom α (Filter α)

        pure as a OneHom.

        Equations
        • Filter.pureOneHom = { toFun := pure, map_one' := (_ : pure 1 = 1) }
        Instances For
          @[simp]
          theorem Filter.coe_pureZeroHom {α : Type u_2} [Zero α] :
          Filter.pureZeroHom = pure
          @[simp]
          theorem Filter.coe_pureOneHom {α : Type u_2} [One α] :
          Filter.pureOneHom = pure
          @[simp]
          theorem Filter.pureZeroHom_apply {α : Type u_2} [Zero α] (a : α) :
          Filter.pureZeroHom a = pure a
          @[simp]
          theorem Filter.pureOneHom_apply {α : Type u_2} [One α] (a : α) :
          Filter.pureOneHom a = pure a
          theorem Filter.map_zero {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [ZeroHomClass F α β] (φ : F) :
          Filter.map (φ) 0 = 0
          theorem Filter.map_one {F : Type u_1} {α : Type u_2} {β : Type u_3} [One α] [One β] [OneHomClass F α β] (φ : F) :
          Filter.map (φ) 1 = 1

          Filter negation/inversion #

          instance Filter.instNeg {α : Type u_2} [Neg α] :
          Neg (Filter α)

          The negation of a filter is the pointwise preimage under - of its sets.

          Equations
          instance Filter.instInv {α : Type u_2} [Inv α] :
          Inv (Filter α)

          The inverse of a filter is the pointwise preimage under ⁻¹ of its sets.

          Equations
          @[simp]
          theorem Filter.map_neg {α : Type u_2} [Neg α] {f : Filter α} :
          Filter.map Neg.neg f = -f
          @[simp]
          theorem Filter.map_inv {α : Type u_2} [Inv α] {f : Filter α} :
          Filter.map Inv.inv f = f⁻¹
          theorem Filter.mem_neg {α : Type u_2} [Neg α] {f : Filter α} {s : Set α} :
          s -f Neg.neg ⁻¹' s f
          theorem Filter.mem_inv {α : Type u_2} [Inv α] {f : Filter α} {s : Set α} :
          s f⁻¹ Inv.inv ⁻¹' s f
          theorem Filter.neg_le_neg {α : Type u_2} [Neg α] {f : Filter α} {g : Filter α} (hf : f g) :
          -f -g
          theorem Filter.inv_le_inv {α : Type u_2} [Inv α] {f : Filter α} {g : Filter α} (hf : f g) :
          @[simp]
          theorem Filter.neg_pure {α : Type u_2} [Neg α] {a : α} :
          -pure a = pure (-a)
          @[simp]
          theorem Filter.inv_pure {α : Type u_2} [Inv α] {a : α} :
          @[simp]
          theorem Filter.neg_eq_bot_iff {α : Type u_2} [Neg α] {f : Filter α} :
          -f = f =
          @[simp]
          theorem Filter.inv_eq_bot_iff {α : Type u_2} [Inv α] {f : Filter α} :
          @[simp]
          theorem Filter.neBot_neg_iff {α : Type u_2} [Neg α] {f : Filter α} :
          @[simp]
          theorem Filter.neBot_inv_iff {α : Type u_2} [Inv α] {f : Filter α} :
          theorem Filter.NeBot.neg {α : Type u_2} [Neg α] {f : Filter α} :
          theorem Filter.NeBot.inv {α : Type u_2} [Inv α] {f : Filter α} :
          theorem Filter.neg_mem_neg {α : Type u_2} [InvolutiveNeg α] {f : Filter α} {s : Set α} (hs : s f) :
          -s -f
          theorem Filter.inv_mem_inv {α : Type u_2} [InvolutiveInv α] {f : Filter α} {s : Set α} (hs : s f) :
          theorem Filter.instInvolutiveNeg.proof_1 {α : Type u_1} [InvolutiveNeg α] (f : Filter α) :
          Filter.map Neg.neg (Filter.map Neg.neg f) = f

          Negation is involutive on Filter α if it is on α.

          Equations
          Instances For

            Inversion is involutive on Filter α if it is on α.

            Equations
            Instances For
              @[simp]
              theorem Filter.neg_le_neg_iff {α : Type u_2} [InvolutiveNeg α] {f : Filter α} {g : Filter α} :
              -f -g f g
              @[simp]
              theorem Filter.inv_le_inv_iff {α : Type u_2} [InvolutiveInv α] {f : Filter α} {g : Filter α} :
              theorem Filter.neg_le_iff_le_neg {α : Type u_2} [InvolutiveNeg α] {f : Filter α} {g : Filter α} :
              -f g f -g
              theorem Filter.inv_le_iff_le_inv {α : Type u_2} [InvolutiveInv α] {f : Filter α} {g : Filter α} :
              @[simp]
              theorem Filter.neg_le_self {α : Type u_2} [InvolutiveNeg α] {f : Filter α} :
              -f f -f = f
              @[simp]
              theorem Filter.inv_le_self {α : Type u_2} [InvolutiveInv α] {f : Filter α} :

              Filter addition/multiplication #

              def Filter.instAdd {α : Type u_2} [Add α] :
              Add (Filter α)

              The filter f + g is generated by {s + t | s ∈ f, t ∈ g} in locale Pointwise.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Filter.instMul {α : Type u_2} [Mul α] :
                Mul (Filter α)

                The filter f * g is generated by {s * t | s ∈ f, t ∈ g} in locale Pointwise.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem Filter.map₂_add {α : Type u_2} [Add α] {f : Filter α} {g : Filter α} :
                  Filter.map₂ (fun x x_1 => x + x_1) f g = f + g
                  @[simp]
                  theorem Filter.map₂_mul {α : Type u_2} [Mul α] {f : Filter α} {g : Filter α} :
                  Filter.map₂ (fun x x_1 => x * x_1) f g = f * g
                  theorem Filter.mem_add {α : Type u_2} [Add α] {f : Filter α} {g : Filter α} {s : Set α} :
                  s f + g t₁ t₂, t₁ f t₂ g t₁ + t₂ s
                  theorem Filter.mem_mul {α : Type u_2} [Mul α] {f : Filter α} {g : Filter α} {s : Set α} :
                  s f * g t₁ t₂, t₁ f t₂ g t₁ * t₂ s
                  theorem Filter.add_mem_add {α : Type u_2} [Add α] {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} :
                  s ft gs + t f + g
                  theorem Filter.mul_mem_mul {α : Type u_2} [Mul α] {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} :
                  s ft gs * t f * g
                  @[simp]
                  theorem Filter.bot_add {α : Type u_2} [Add α] {g : Filter α} :
                  @[simp]
                  theorem Filter.bot_mul {α : Type u_2} [Mul α] {g : Filter α} :
                  @[simp]
                  theorem Filter.add_bot {α : Type u_2} [Add α] {f : Filter α} :
                  @[simp]
                  theorem Filter.mul_bot {α : Type u_2} [Mul α] {f : Filter α} :
                  @[simp]
                  theorem Filter.add_eq_bot_iff {α : Type u_2} [Add α] {f : Filter α} {g : Filter α} :
                  f + g = f = g =
                  @[simp]
                  theorem Filter.mul_eq_bot_iff {α : Type u_2} [Mul α] {f : Filter α} {g : Filter α} :
                  f * g = f = g =
                  @[simp]
                  theorem Filter.add_neBot_iff {α : Type u_2} [Add α] {f : Filter α} {g : Filter α} :
                  @[simp]
                  theorem Filter.mul_neBot_iff {α : Type u_2} [Mul α] {f : Filter α} {g : Filter α} :
                  theorem Filter.NeBot.add {α : Type u_2} [Add α] {f : Filter α} {g : Filter α} :
                  theorem Filter.NeBot.mul {α : Type u_2} [Mul α] {f : Filter α} {g : Filter α} :
                  theorem Filter.NeBot.of_add_left {α : Type u_2} [Add α] {f : Filter α} {g : Filter α} :
                  theorem Filter.NeBot.of_mul_left {α : Type u_2} [Mul α] {f : Filter α} {g : Filter α} :
                  theorem Filter.NeBot.of_add_right {α : Type u_2} [Add α] {f : Filter α} {g : Filter α} :
                  theorem Filter.NeBot.of_mul_right {α : Type u_2} [Mul α] {f : Filter α} {g : Filter α} :
                  @[simp]
                  theorem Filter.pure_add {α : Type u_2} [Add α] {g : Filter α} {a : α} :
                  pure a + g = Filter.map ((fun x x_1 => x + x_1) a) g
                  @[simp]
                  theorem Filter.pure_mul {α : Type u_2} [Mul α] {g : Filter α} {a : α} :
                  pure a * g = Filter.map ((fun x x_1 => x * x_1) a) g
                  @[simp]
                  theorem Filter.add_pure {α : Type u_2} [Add α] {f : Filter α} {b : α} :
                  f + pure b = Filter.map (fun x => x + b) f
                  @[simp]
                  theorem Filter.mul_pure {α : Type u_2} [Mul α] {f : Filter α} {b : α} :
                  f * pure b = Filter.map (fun x => x * b) f
                  theorem Filter.pure_add_pure {α : Type u_2} [Add α] {a : α} {b : α} :
                  pure a + pure b = pure (a + b)
                  theorem Filter.pure_mul_pure {α : Type u_2} [Mul α] {a : α} {b : α} :
                  pure a * pure b = pure (a * b)
                  @[simp]
                  theorem Filter.le_add_iff {α : Type u_2} [Add α] {f : Filter α} {g : Filter α} {h : Filter α} :
                  h f + g ∀ ⦃s : Set α⦄, s f∀ ⦃t : Set α⦄, t gs + t h
                  @[simp]
                  theorem Filter.le_mul_iff {α : Type u_2} [Mul α] {f : Filter α} {g : Filter α} {h : Filter α} :
                  h f * g ∀ ⦃s : Set α⦄, s f∀ ⦃t : Set α⦄, t gs * t h
                  theorem Filter.covariant_add.proof_1 {α : Type u_1} [Add α] :
                  CovariantClass (Filter α) (Filter α) (fun x x_1 => x + x_1) fun x x_1 => x x_1
                  instance Filter.covariant_add {α : Type u_2} [Add α] :
                  CovariantClass (Filter α) (Filter α) (fun x x_1 => x + x_1) fun x x_1 => x x_1
                  Equations
                  instance Filter.covariant_mul {α : Type u_2} [Mul α] :
                  CovariantClass (Filter α) (Filter α) (fun x x_1 => x * x_1) fun x x_1 => x x_1
                  Equations
                  theorem Filter.covariant_swap_add.proof_1 {α : Type u_1} [Add α] :
                  CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
                  instance Filter.covariant_swap_add {α : Type u_2} [Add α] :
                  CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
                  Equations
                  instance Filter.covariant_swap_mul {α : Type u_2} [Mul α] :
                  CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1
                  Equations
                  theorem Filter.map_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] {f₁ : Filter α} {f₂ : Filter α} [AddHomClass F α β] (m : F) :
                  Filter.map (m) (f₁ + f₂) = Filter.map (m) f₁ + Filter.map (m) f₂
                  theorem Filter.map_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] {f₁ : Filter α} {f₂ : Filter α} [MulHomClass F α β] (m : F) :
                  Filter.map (m) (f₁ * f₂) = Filter.map (m) f₁ * Filter.map (m) f₂
                  def Filter.pureAddHom {α : Type u_2} [Add α] :
                  AddHom α (Filter α)

                  The singleton operation as an AddHom.

                  Equations
                  • Filter.pureAddHom = { toFun := pure, map_add' := (_ : ∀ (x x_1 : α), pure (x + x_1) = pure x + pure x_1) }
                  Instances For
                    theorem Filter.pureAddHom.proof_1 {α : Type u_1} [Add α] :
                    ∀ (x x_1 : α), pure (x + x_1) = pure x + pure x_1
                    def Filter.pureMulHom {α : Type u_2} [Mul α] :

                    pure operation as a MulHom.

                    Equations
                    • Filter.pureMulHom = { toFun := pure, map_mul' := (_ : ∀ (x x_1 : α), pure (x * x_1) = pure x * pure x_1) }
                    Instances For
                      @[simp]
                      theorem Filter.coe_pureAddHom {α : Type u_2} [Add α] :
                      Filter.pureAddHom = pure
                      @[simp]
                      theorem Filter.coe_pureMulHom {α : Type u_2} [Mul α] :
                      Filter.pureMulHom = pure
                      @[simp]
                      theorem Filter.pureAddHom_apply {α : Type u_2} [Add α] (a : α) :
                      Filter.pureAddHom a = pure a
                      @[simp]
                      theorem Filter.pureMulHom_apply {α : Type u_2} [Mul α] (a : α) :
                      Filter.pureMulHom a = pure a

                      Filter subtraction/division #

                      def Filter.instSub {α : Type u_2} [Sub α] :
                      Sub (Filter α)

                      The filter f - g is generated by {s - t | s ∈ f, t ∈ g} in locale Pointwise.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Filter.instDiv {α : Type u_2} [Div α] :
                        Div (Filter α)

                        The filter f / g is generated by {s / t | s ∈ f, t ∈ g} in locale Pointwise.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem Filter.map₂_sub {α : Type u_2} [Sub α] {f : Filter α} {g : Filter α} :
                          Filter.map₂ (fun x x_1 => x - x_1) f g = f - g
                          @[simp]
                          theorem Filter.map₂_div {α : Type u_2} [Div α] {f : Filter α} {g : Filter α} :
                          Filter.map₂ (fun x x_1 => x / x_1) f g = f / g
                          theorem Filter.mem_sub {α : Type u_2} [Sub α] {f : Filter α} {g : Filter α} {s : Set α} :
                          s f - g t₁ t₂, t₁ f t₂ g t₁ - t₂ s
                          theorem Filter.mem_div {α : Type u_2} [Div α] {f : Filter α} {g : Filter α} {s : Set α} :
                          s f / g t₁ t₂, t₁ f t₂ g t₁ / t₂ s
                          theorem Filter.sub_mem_sub {α : Type u_2} [Sub α] {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} :
                          s ft gs - t f - g
                          theorem Filter.div_mem_div {α : Type u_2} [Div α] {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} :
                          s ft gs / t f / g
                          @[simp]
                          theorem Filter.bot_sub {α : Type u_2} [Sub α] {g : Filter α} :
                          @[simp]
                          theorem Filter.bot_div {α : Type u_2} [Div α] {g : Filter α} :
                          @[simp]
                          theorem Filter.sub_bot {α : Type u_2} [Sub α] {f : Filter α} :
                          @[simp]
                          theorem Filter.div_bot {α : Type u_2} [Div α] {f : Filter α} :
                          @[simp]
                          theorem Filter.sub_eq_bot_iff {α : Type u_2} [Sub α] {f : Filter α} {g : Filter α} :
                          f - g = f = g =
                          @[simp]
                          theorem Filter.div_eq_bot_iff {α : Type u_2} [Div α] {f : Filter α} {g : Filter α} :
                          f / g = f = g =
                          @[simp]
                          theorem Filter.sub_neBot_iff {α : Type u_2} [Sub α] {f : Filter α} {g : Filter α} :
                          @[simp]
                          theorem Filter.div_neBot_iff {α : Type u_2} [Div α] {f : Filter α} {g : Filter α} :
                          theorem Filter.NeBot.sub {α : Type u_2} [Sub α] {f : Filter α} {g : Filter α} :
                          theorem Filter.NeBot.div {α : Type u_2} [Div α] {f : Filter α} {g : Filter α} :
                          theorem Filter.NeBot.of_sub_left {α : Type u_2} [Sub α] {f : Filter α} {g : Filter α} :
                          theorem Filter.NeBot.of_div_left {α : Type u_2} [Div α] {f : Filter α} {g : Filter α} :
                          theorem Filter.NeBot.of_sub_right {α : Type u_2} [Sub α] {f : Filter α} {g : Filter α} :
                          theorem Filter.NeBot.of_div_right {α : Type u_2} [Div α] {f : Filter α} {g : Filter α} :
                          @[simp]
                          theorem Filter.pure_sub {α : Type u_2} [Sub α] {g : Filter α} {a : α} :
                          pure a - g = Filter.map ((fun x x_1 => x - x_1) a) g
                          @[simp]
                          theorem Filter.pure_div {α : Type u_2} [Div α] {g : Filter α} {a : α} :
                          pure a / g = Filter.map ((fun x x_1 => x / x_1) a) g
                          @[simp]
                          theorem Filter.sub_pure {α : Type u_2} [Sub α] {f : Filter α} {b : α} :
                          f - pure b = Filter.map (fun x => x - b) f
                          @[simp]
                          theorem Filter.div_pure {α : Type u_2} [Div α] {f : Filter α} {b : α} :
                          f / pure b = Filter.map (fun x => x / b) f
                          theorem Filter.pure_sub_pure {α : Type u_2} [Sub α] {a : α} {b : α} :
                          pure a - pure b = pure (a - b)
                          theorem Filter.pure_div_pure {α : Type u_2} [Div α] {a : α} {b : α} :
                          pure a / pure b = pure (a / b)
                          theorem Filter.sub_le_sub {α : Type u_2} [Sub α] {f₁ : Filter α} {f₂ : Filter α} {g₁ : Filter α} {g₂ : Filter α} :
                          f₁ f₂g₁ g₂f₁ - g₁ f₂ - g₂
                          theorem Filter.div_le_div {α : Type u_2} [Div α] {f₁ : Filter α} {f₂ : Filter α} {g₁ : Filter α} {g₂ : Filter α} :
                          f₁ f₂g₁ g₂f₁ / g₁ f₂ / g₂
                          theorem Filter.sub_le_sub_left {α : Type u_2} [Sub α] {f : Filter α} {g₁ : Filter α} {g₂ : Filter α} :
                          g₁ g₂f - g₁ f - g₂
                          theorem Filter.div_le_div_left {α : Type u_2} [Div α] {f : Filter α} {g₁ : Filter α} {g₂ : Filter α} :
                          g₁ g₂f / g₁ f / g₂
                          theorem Filter.sub_le_sub_right {α : Type u_2} [Sub α] {f₁ : Filter α} {f₂ : Filter α} {g : Filter α} :
                          f₁ f₂f₁ - g f₂ - g
                          theorem Filter.div_le_div_right {α : Type u_2} [Div α] {f₁ : Filter α} {f₂ : Filter α} {g : Filter α} :
                          f₁ f₂f₁ / g f₂ / g
                          @[simp]
                          theorem Filter.le_sub_iff {α : Type u_2} [Sub α] {f : Filter α} {g : Filter α} {h : Filter α} :
                          h f - g ∀ ⦃s : Set α⦄, s f∀ ⦃t : Set α⦄, t gs - t h
                          @[simp]
                          theorem Filter.le_div_iff {α : Type u_2} [Div α] {f : Filter α} {g : Filter α} {h : Filter α} :
                          h f / g ∀ ⦃s : Set α⦄, s f∀ ⦃t : Set α⦄, t gs / t h
                          instance Filter.covariant_sub {α : Type u_2} [Sub α] :
                          CovariantClass (Filter α) (Filter α) (fun x x_1 => x - x_1) fun x x_1 => x x_1
                          Equations
                          theorem Filter.covariant_sub.proof_1 {α : Type u_1} [Sub α] :
                          CovariantClass (Filter α) (Filter α) (fun x x_1 => x - x_1) fun x x_1 => x x_1
                          instance Filter.covariant_div {α : Type u_2} [Div α] :
                          CovariantClass (Filter α) (Filter α) (fun x x_1 => x / x_1) fun x x_1 => x x_1
                          Equations
                          theorem Filter.covariant_swap_sub.proof_1 {α : Type u_1} [Sub α] :
                          CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x - x_1) fun x x_1 => x x_1
                          instance Filter.covariant_swap_sub {α : Type u_2} [Sub α] :
                          CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x - x_1) fun x x_1 => x x_1
                          Equations
                          instance Filter.covariant_swap_div {α : Type u_2} [Div α] :
                          CovariantClass (Filter α) (Filter α) (Function.swap fun x x_1 => x / x_1) fun x x_1 => x x_1
                          Equations
                          def Filter.instNSMul {α : Type u_2} [Zero α] [Add α] :

                          Repeated pointwise addition (not the same as pointwise repeated addition!) of a Filter. See Note [pointwise nat action].

                          Equations
                          • Filter.instNSMul = { smul := nsmulRec }
                          Instances For
                            def Filter.instNPow {α : Type u_2} [One α] [Mul α] :

                            Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a Filter. See Note [pointwise nat action].

                            Equations
                            • Filter.instNPow = { pow := fun s n => npowRec n s }
                            Instances For
                              def Filter.instZSMul {α : Type u_2} [Zero α] [Add α] [Neg α] :

                              Repeated pointwise addition/subtraction (not the same as pointwise repeated addition/subtraction!) of a Filter. See Note [pointwise nat action].

                              Equations
                              • Filter.instZSMul = { smul := zsmulRec }
                              Instances For
                                def Filter.instZPow {α : Type u_2} [One α] [Mul α] [Inv α] :

                                Repeated pointwise multiplication/division (not the same as pointwise repeated multiplication/division!) of a Filter. See Note [pointwise nat action].

                                Equations
                                • Filter.instZPow = { pow := fun s n => zpowRec n s }
                                Instances For
                                  theorem Filter.addSemigroup.proof_1 {α : Type u_1} [AddSemigroup α] :
                                  ∀ (x x_1 x_2 : Filter α), Filter.map₂ (fun x x_3 => x + x_3) (Filter.map₂ (fun x x_3 => x + x_3) x x_1) x_2 = Filter.map₂ (fun x x_3 => x + x_3) x (Filter.map₂ (fun x x_3 => x + x_3) x_1 x_2)

                                  Filter α is an AddSemigroup under pointwise operations if α is.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def Filter.semigroup {α : Type u_2} [Semigroup α] :

                                    Filter α is a Semigroup under pointwise operations if α is.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem Filter.addCommSemigroup.proof_1 {α : Type u_1} [AddCommSemigroup α] (a : Filter α) (b : Filter α) (c : Filter α) :
                                      a + b + c = a + (b + c)

                                      Filter α is an AddCommSemigroup under pointwise operations if α is.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem Filter.addCommSemigroup.proof_2 {α : Type u_1} [AddCommSemigroup α] :
                                        ∀ (x x_1 : Filter α), Filter.map₂ (fun x x_2 => x + x_2) x x_1 = Filter.map₂ (fun x x_2 => x + x_2) x_1 x

                                        Filter α is a CommSemigroup under pointwise operations if α is.

                                        Equations
                                        Instances For
                                          theorem Filter.addZeroClass.proof_1 {α : Type u_1} [AddZeroClass α] (l : Filter α) :
                                          Filter.map₂ (fun x x_1 => x + x_1) (pure 0) l = l

                                          Filter α is an AddZeroClass under pointwise operations if α is.

                                          Equations
                                          Instances For
                                            theorem Filter.addZeroClass.proof_2 {α : Type u_1} [AddZeroClass α] (l : Filter α) :
                                            Filter.map₂ (fun x x_1 => x + x_1) l (pure 0) = l

                                            Filter α is a MulOneClass under pointwise operations if α is.

                                            Equations
                                            Instances For
                                              theorem Filter.mapAddMonoidHom.proof_2 {F : Type u_3} {α : Type u_1} {β : Type u_2} [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (φ : F) :
                                              ∀ (x x_1 : Filter α), Filter.map (φ) (x + x_1) = Filter.map (φ) x + Filter.map (φ) x_1
                                              def Filter.mapAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (φ : F) :

                                              If φ : α →+ β then mapAddMonoidHom φ is the monoid homomorphism Filter α →+ Filter β induced by map φ.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem Filter.mapAddMonoidHom.proof_1 {F : Type u_3} {α : Type u_2} {β : Type u_1} [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] (φ : F) :
                                                Filter.map (φ) 0 = 0
                                                def Filter.mapMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass α] [MulOneClass β] [MonoidHomClass F α β] (φ : F) :

                                                If φ : α →* β then mapMonoidHom φ is the monoid homomorphism Filter α →* Filter β induced by map φ.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  theorem Filter.comap_add_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [AddHomClass F α β] (m : F) {f : Filter β} {g : Filter β} :
                                                  Filter.comap (m) f + Filter.comap (m) g Filter.comap (m) (f + g)
                                                  abbrev Filter.comap_add_comap_le.match_1 {F : Type u_3} {α : Type u_1} {β : Type u_2} [AddZeroClass α] [AddZeroClass β] [AddHomClass F α β] (m : F) {f : Filter β} {g : Filter β} :
                                                  ∀ (x : Set α) (motive : x Filter.comap (m) (f + g)Prop) (x_1 : x Filter.comap (m) (f + g)), (∀ (w t₁ t₂ : Set β) (ht₁ : t₁ f) (ht₂ : t₂ g) (t₁t₂ : t₁ + t₂ w) (mt : m ⁻¹' w x), motive (_ : t, t f + g m ⁻¹' t x)) → motive x_1
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    theorem Filter.comap_mul_comap_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass α] [MulOneClass β] [MulHomClass F α β] (m : F) {f : Filter β} {g : Filter β} :
                                                    Filter.comap (m) f * Filter.comap (m) g Filter.comap (m) (f * g)
                                                    theorem Filter.Tendsto.add_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [AddHomClass F α β] (m : F) {f₁ : Filter α} {g₁ : Filter α} {f₂ : Filter β} {g₂ : Filter β} :
                                                    Filter.Tendsto (m) f₁ f₂Filter.Tendsto (m) g₁ g₂Filter.Tendsto (m) (f₁ + g₁) (f₂ + g₂)
                                                    theorem Filter.Tendsto.mul_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass α] [MulOneClass β] [MulHomClass F α β] (m : F) {f₁ : Filter α} {g₁ : Filter α} {f₂ : Filter β} {g₂ : Filter β} :
                                                    Filter.Tendsto (m) f₁ f₂Filter.Tendsto (m) g₁ g₂Filter.Tendsto (m) (f₁ * g₁) (f₂ * g₂)
                                                    theorem Filter.pureAddMonoidHom.proof_2 {α : Type u_1} [AddZeroClass α] (x : α) (y : α) :
                                                    AddHom.toFun Filter.pureAddHom (x + y) = AddHom.toFun Filter.pureAddHom x + AddHom.toFun Filter.pureAddHom y
                                                    theorem Filter.pureAddMonoidHom.proof_1 {α : Type u_1} [AddZeroClass α] :
                                                    ZeroHom.toFun Filter.pureZeroHom 0 = 0

                                                    pure as an AddMonoidHom.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      def Filter.pureMonoidHom {α : Type u_2} [MulOneClass α] :
                                                      α →* Filter α

                                                      pure as a MonoidHom.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        theorem Filter.coe_pureAddMonoidHom {α : Type u_2} [AddZeroClass α] :
                                                        Filter.pureAddMonoidHom = pure
                                                        @[simp]
                                                        theorem Filter.coe_pureMonoidHom {α : Type u_2} [MulOneClass α] :
                                                        Filter.pureMonoidHom = pure
                                                        @[simp]
                                                        theorem Filter.pureAddMonoidHom_apply {α : Type u_2} [AddZeroClass α] (a : α) :
                                                        Filter.pureAddMonoidHom a = pure a
                                                        @[simp]
                                                        theorem Filter.pureMonoidHom_apply {α : Type u_2} [MulOneClass α] (a : α) :
                                                        Filter.pureMonoidHom a = pure a
                                                        theorem Filter.addMonoid.proof_2 {α : Type u_1} [AddMonoid α] (a : Filter α) :
                                                        0 + a = a
                                                        def Filter.addMonoid {α : Type u_2} [AddMonoid α] :

                                                        Filter α is an AddMonoid under pointwise operations if α is.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          theorem Filter.addMonoid.proof_4 {α : Type u_1} [AddMonoid α] :
                                                          ∀ (x : Filter α), nsmulRec 0 x = nsmulRec 0 x
                                                          theorem Filter.addMonoid.proof_1 {α : Type u_1} [AddMonoid α] (a : Filter α) (b : Filter α) (c : Filter α) :
                                                          a + b + c = a + (b + c)
                                                          theorem Filter.addMonoid.proof_5 {α : Type u_1} [AddMonoid α] :
                                                          ∀ (n : ) (x : Filter α), nsmulRec (n + 1) x = nsmulRec (n + 1) x
                                                          theorem Filter.addMonoid.proof_3 {α : Type u_1} [AddMonoid α] (a : Filter α) :
                                                          a + 0 = a
                                                          def Filter.monoid {α : Type u_2} [Monoid α] :

                                                          Filter α is a Monoid under pointwise operations if α is.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            theorem Filter.nsmul_mem_nsmul {α : Type u_2} [AddMonoid α] {f : Filter α} {s : Set α} (hs : s f) (n : ) :
                                                            n s n f
                                                            abbrev Filter.nsmul_mem_nsmul.match_1 (motive : Prop) :
                                                            (x : ) → (Unitmotive 0) → ((n : ) → motive (Nat.succ n)) → motive x
                                                            Equations
                                                            Instances For
                                                              theorem Filter.pow_mem_pow {α : Type u_2} [Monoid α] {f : Filter α} {s : Set α} (hs : s f) (n : ) :
                                                              s ^ n f ^ n
                                                              @[simp]
                                                              theorem Filter.nsmul_bot {α : Type u_2} [AddMonoid α] {n : } (hn : n 0) :
                                                              @[simp]
                                                              theorem Filter.bot_pow {α : Type u_2} [Monoid α] {n : } (hn : n 0) :
                                                              theorem Filter.add_top_of_nonneg {α : Type u_2} [AddMonoid α] {f : Filter α} (hf : 0 f) :
                                                              theorem Filter.mul_top_of_one_le {α : Type u_2} [Monoid α] {f : Filter α} (hf : 1 f) :
                                                              theorem Filter.top_add_of_nonneg {α : Type u_2} [AddMonoid α] {f : Filter α} (hf : 0 f) :
                                                              theorem Filter.top_mul_of_one_le {α : Type u_2} [Monoid α] {f : Filter α} (hf : 1 f) :
                                                              @[simp]
                                                              theorem Filter.top_add_top {α : Type u_2} [AddMonoid α] :
                                                              @[simp]
                                                              theorem Filter.top_mul_top {α : Type u_2} [Monoid α] :
                                                              theorem Filter.nsmul_top {α : Type u_2} [AddMonoid α] {n : } :
                                                              n 0n =
                                                              abbrev Filter.nsmul_top.match_1 (motive : Prop) :
                                                              (x : ) → (Unitmotive 0) → (Unitmotive 1) → ((n : ) → motive (Nat.succ (Nat.succ n))) → motive x
                                                              Equations
                                                              Instances For
                                                                theorem Filter.top_pow {α : Type u_2} [Monoid α] {n : } :
                                                                n 0 ^ n =
                                                                theorem IsAddUnit.filter {α : Type u_2} [AddMonoid α] {a : α} :
                                                                theorem IsUnit.filter {α : Type u_2} [Monoid α] {a : α} :
                                                                IsUnit aIsUnit (pure a)
                                                                theorem Filter.addCommMonoid.proof_2 {α : Type u_1} [AddCommMonoid α] (a : Filter α) :
                                                                a + 0 = a

                                                                Filter α is an AddCommMonoid under pointwise operations if α is.

                                                                Equations
                                                                • Filter.addCommMonoid = let src := Filter.addZeroClass; let src_1 := Filter.addCommSemigroup; AddCommMonoid.mk (_ : ∀ (a b : Filter α), a + b = b + a)
                                                                Instances For
                                                                  theorem Filter.addCommMonoid.proof_3 {α : Type u_1} [AddCommMonoid α] :
                                                                  ∀ (x : Filter α), nsmulRec 0 x = nsmulRec 0 x
                                                                  theorem Filter.addCommMonoid.proof_1 {α : Type u_1} [AddCommMonoid α] (a : Filter α) :
                                                                  0 + a = a
                                                                  theorem Filter.addCommMonoid.proof_5 {α : Type u_1} [AddCommMonoid α] (a : Filter α) (b : Filter α) :
                                                                  a + b = b + a
                                                                  theorem Filter.addCommMonoid.proof_4 {α : Type u_1} [AddCommMonoid α] :
                                                                  ∀ (n : ) (x : Filter α), nsmulRec (n + 1) x = nsmulRec (n + 1) x

                                                                  Filter α is a CommMonoid under pointwise operations if α is.

                                                                  Equations
                                                                  • Filter.commMonoid = let src := Filter.mulOneClass; let src_1 := Filter.commSemigroup; CommMonoid.mk (_ : ∀ (a b : Filter α), a * b = b * a)
                                                                  Instances For
                                                                    theorem Filter.add_eq_zero_iff {α : Type u_2} [SubtractionMonoid α] {f : Filter α} {g : Filter α} :
                                                                    f + g = 0 a b, f = pure a g = pure b a + b = 0
                                                                    theorem Filter.mul_eq_one_iff {α : Type u_2} [DivisionMonoid α] {f : Filter α} {g : Filter α} :
                                                                    f * g = 1 a b, f = pure a g = pure b a * b = 1
                                                                    theorem Filter.subtractionMonoid.proof_2 {α : Type u_1} [SubtractionMonoid α] (a : Filter α) :
                                                                    a + 0 = a
                                                                    theorem Filter.subtractionMonoid.proof_12 {α : Type u_1} [SubtractionMonoid α] (s : Filter α) (t : Filter α) (h : s + t = 0) :
                                                                    -s = t
                                                                    theorem Filter.subtractionMonoid.proof_9 {α : Type u_1} [SubtractionMonoid α] :
                                                                    ∀ (n : ) (a : Filter α), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a
                                                                    theorem Filter.subtractionMonoid.proof_7 {α : Type u_1} [SubtractionMonoid α] :
                                                                    ∀ (a : Filter α), zsmulRec 0 a = zsmulRec 0 a
                                                                    theorem Filter.subtractionMonoid.proof_5 {α : Type u_1} [SubtractionMonoid α] (f : Filter α) (g : Filter α) :
                                                                    Filter.map (fun x => x) (Filter.map₂ (fun x x_1 => x - x_1) f g) = Filter.map₂ (fun x x_1 => x + x_1) f (Filter.map Neg.neg g)
                                                                    theorem Filter.subtractionMonoid.proof_6 {α : Type u_1} [SubtractionMonoid α] (a : Filter α) (b : Filter α) (c : Filter α) :
                                                                    a + b + c = a + (b + c)
                                                                    theorem Filter.subtractionMonoid.proof_11 {α : Type u_1} [SubtractionMonoid α] (s : Filter α) (t : Filter α) :
                                                                    Filter.map Neg.neg (Filter.map₂ (fun x x_1 => x + x_1) s t) = Filter.map₂ (fun x x_1 => x + x_1) (Filter.map Neg.neg t) (Filter.map Neg.neg s)

                                                                    Filter α is a subtraction monoid under pointwise operations if α is.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      theorem Filter.subtractionMonoid.proof_8 {α : Type u_1} [SubtractionMonoid α] :
                                                                      ∀ (n : ) (a : Filter α), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a
                                                                      theorem Filter.subtractionMonoid.proof_1 {α : Type u_1} [SubtractionMonoid α] (a : Filter α) :
                                                                      0 + a = a

                                                                      Filter α is a division monoid under pointwise operations if α is.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        theorem Filter.isAddUnit_iff {α : Type u_2} [SubtractionMonoid α] {f : Filter α} :
                                                                        IsAddUnit f a, f = pure a IsAddUnit a
                                                                        theorem Filter.isUnit_iff {α : Type u_2} [DivisionMonoid α] {f : Filter α} :
                                                                        IsUnit f a, f = pure a IsUnit a
                                                                        theorem Filter.subtractionCommMonoid.proof_2 {α : Type u_1} [SubtractionCommMonoid α] (a : Filter α) (b : Filter α) :
                                                                        -(a + b) = -b + -a
                                                                        theorem Filter.subtractionCommMonoid.proof_4 {α : Type u_1} [SubtractionCommMonoid α] (a : Filter α) (b : Filter α) :
                                                                        a + b = b + a
                                                                        theorem Filter.subtractionCommMonoid.proof_3 {α : Type u_1} [SubtractionCommMonoid α] (a : Filter α) (b : Filter α) :
                                                                        a + b = 0-a = b

                                                                        Filter α is a commutative subtraction monoid under pointwise operations if α is.

                                                                        Equations
                                                                        • Filter.subtractionCommMonoid = let src := Filter.subtractionMonoid; let src_1 := Filter.addCommSemigroup; SubtractionCommMonoid.mk (_ : ∀ (a b : Filter α), a + b = b + a)
                                                                        Instances For

                                                                          Filter α is a commutative division monoid under pointwise operations if α is.

                                                                          Equations
                                                                          • Filter.divisionCommMonoid = let src := Filter.divisionMonoid; let src_1 := Filter.commSemigroup; DivisionCommMonoid.mk (_ : ∀ (a b : Filter α), a * b = b * a)
                                                                          Instances For

                                                                            Filter α has distributive negation if α has.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For

                                                                              Note that Filter α is not a Distrib because f * g + f * h has cross terms that f * (g + h) lacks.

                                                                              theorem Filter.mul_add_subset {α : Type u_2} [Distrib α] {f : Filter α} {g : Filter α} {h : Filter α} :
                                                                              f * (g + h) f * g + f * h
                                                                              theorem Filter.add_mul_subset {α : Type u_2} [Distrib α] {f : Filter α} {g : Filter α} {h : Filter α} :
                                                                              (f + g) * h f * h + g * h

                                                                              Note that Filter is not a MulZeroClass because 0 * ⊥ ≠ 0.

                                                                              theorem Filter.NeBot.mul_zero_nonneg {α : Type u_2} [MulZeroClass α] {f : Filter α} (hf : Filter.NeBot f) :
                                                                              0 f * 0
                                                                              theorem Filter.NeBot.zero_mul_nonneg {α : Type u_2} [MulZeroClass α] {g : Filter α} (hg : Filter.NeBot g) :
                                                                              0 0 * g

                                                                              Note that Filter α is not a group because f / f ≠ 1 in general

                                                                              @[simp]
                                                                              theorem Filter.nonneg_sub_iff {α : Type u_2} [AddGroup α] {f : Filter α} {g : Filter α} :
                                                                              0 f - g ¬Disjoint f g
                                                                              @[simp]
                                                                              theorem Filter.one_le_div_iff {α : Type u_2} [Group α] {f : Filter α} {g : Filter α} :
                                                                              1 f / g ¬Disjoint f g
                                                                              theorem Filter.not_nonneg_sub_iff {α : Type u_2} [AddGroup α] {f : Filter α} {g : Filter α} :
                                                                              ¬0 f - g Disjoint f g
                                                                              theorem Filter.not_one_le_div_iff {α : Type u_2} [Group α] {f : Filter α} {g : Filter α} :
                                                                              ¬1 f / g Disjoint f g
                                                                              theorem Filter.NeBot.nonneg_sub {α : Type u_2} [AddGroup α] {f : Filter α} (h : Filter.NeBot f) :
                                                                              0 f - f
                                                                              theorem Filter.NeBot.one_le_div {α : Type u_2} [Group α] {f : Filter α} (h : Filter.NeBot f) :
                                                                              1 f / f
                                                                              theorem Filter.isAddUnit_pure {α : Type u_2} [AddGroup α] (a : α) :
                                                                              theorem Filter.isUnit_pure {α : Type u_2} [Group α] (a : α) :
                                                                              @[simp]
                                                                              theorem Filter.isUnit_iff_singleton {α : Type u_2} [Group α] {f : Filter α} :
                                                                              IsUnit f a, f = pure a
                                                                              theorem Filter.map_neg' {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [AddMonoidHomClass F α β] (m : F) {f : Filter α} :
                                                                              Filter.map (m) (-f) = -Filter.map (m) f
                                                                              theorem Filter.map_inv' {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [MonoidHomClass F α β] (m : F) {f : Filter α} :
                                                                              Filter.map (m) f⁻¹ = (Filter.map (m) f)⁻¹
                                                                              theorem Filter.Tendsto.neg_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [AddMonoidHomClass F α β] (m : F) {f₁ : Filter α} {f₂ : Filter β} :
                                                                              Filter.Tendsto (m) f₁ f₂Filter.Tendsto (m) (-f₁) (-f₂)
                                                                              theorem Filter.Tendsto.inv_inv {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [MonoidHomClass F α β] (m : F) {f₁ : Filter α} {f₂ : Filter β} :
                                                                              Filter.Tendsto (m) f₁ f₂Filter.Tendsto (m) f₁⁻¹ f₂⁻¹
                                                                              theorem Filter.map_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [AddMonoidHomClass F α β] (m : F) {f : Filter α} {g : Filter α} :
                                                                              Filter.map (m) (f - g) = Filter.map (m) f - Filter.map (m) g
                                                                              theorem Filter.map_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [MonoidHomClass F α β] (m : F) {f : Filter α} {g : Filter α} :
                                                                              Filter.map (m) (f / g) = Filter.map (m) f / Filter.map (m) g
                                                                              theorem Filter.Tendsto.sub_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [AddMonoidHomClass F α β] (m : F) {f₁ : Filter α} {g₁ : Filter α} {f₂ : Filter β} {g₂ : Filter β} (hf : Filter.Tendsto (m) f₁ f₂) (hg : Filter.Tendsto (m) g₁ g₂) :
                                                                              Filter.Tendsto (m) (f₁ - g₁) (f₂ - g₂)
                                                                              theorem Filter.Tendsto.div_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [MonoidHomClass F α β] (m : F) {f₁ : Filter α} {g₁ : Filter α} {f₂ : Filter β} {g₂ : Filter β} (hf : Filter.Tendsto (m) f₁ f₂) (hg : Filter.Tendsto (m) g₁ g₂) :
                                                                              Filter.Tendsto (m) (f₁ / g₁) (f₂ / g₂)
                                                                              theorem Filter.NeBot.div_zero_nonneg {α : Type u_2} [GroupWithZero α] {f : Filter α} (hf : Filter.NeBot f) :
                                                                              0 f / 0
                                                                              theorem Filter.NeBot.zero_div_nonneg {α : Type u_2} [GroupWithZero α] {g : Filter α} (hg : Filter.NeBot g) :
                                                                              0 0 / g

                                                                              Scalar addition/multiplication of filters #

                                                                              def Filter.instVAdd {α : Type u_2} {β : Type u_3} [VAdd α β] :
                                                                              VAdd (Filter α) (Filter β)

                                                                              The filter f +ᵥ g is generated by {s +ᵥ t | s ∈ f, t ∈ g} in locale Pointwise.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                def Filter.instSMul {α : Type u_2} {β : Type u_3} [SMul α β] :
                                                                                SMul (Filter α) (Filter β)

                                                                                The filter f • g is generated by {s • t | s ∈ f, t ∈ g} in locale Pointwise.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem Filter.map₂_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} :
                                                                                  Filter.map₂ (fun x x_1 => x +ᵥ x_1) f g = f +ᵥ g
                                                                                  @[simp]
                                                                                  theorem Filter.map₂_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} :
                                                                                  Filter.map₂ (fun x x_1 => x x_1) f g = f g
                                                                                  theorem Filter.mem_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} {t : Set β} :
                                                                                  t f +ᵥ g t₁ t₂, t₁ f t₂ g t₁ +ᵥ t₂ t
                                                                                  theorem Filter.mem_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} {t : Set β} :
                                                                                  t f g t₁ t₂, t₁ f t₂ g t₁ t₂ t
                                                                                  theorem Filter.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} {s : Set α} {t : Set β} :
                                                                                  s ft gs +ᵥ t f +ᵥ g
                                                                                  theorem Filter.smul_mem_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} {s : Set α} {t : Set β} :
                                                                                  s ft gs t f g
                                                                                  @[simp]
                                                                                  theorem Filter.bot_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {g : Filter β} :
                                                                                  @[simp]
                                                                                  theorem Filter.bot_smul {α : Type u_2} {β : Type u_3} [SMul α β] {g : Filter β} :
                                                                                  @[simp]
                                                                                  theorem Filter.vadd_bot {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} :
                                                                                  @[simp]
                                                                                  theorem Filter.smul_bot {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} :
                                                                                  @[simp]
                                                                                  theorem Filter.vadd_eq_bot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} :
                                                                                  f +ᵥ g = f = g =
                                                                                  @[simp]
                                                                                  theorem Filter.smul_eq_bot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} :
                                                                                  f g = f = g =
                                                                                  @[simp]
                                                                                  theorem Filter.vadd_neBot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} :
                                                                                  @[simp]
                                                                                  theorem Filter.smul_neBot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} :
                                                                                  theorem Filter.NeBot.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} :
                                                                                  theorem Filter.NeBot.smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} :
                                                                                  theorem Filter.NeBot.of_vadd_left {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} :
                                                                                  theorem Filter.NeBot.of_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} :
                                                                                  theorem Filter.NeBot.of_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} :
                                                                                  theorem Filter.NeBot.of_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} :
                                                                                  @[simp]
                                                                                  theorem Filter.pure_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {g : Filter β} {a : α} :
                                                                                  pure a +ᵥ g = Filter.map ((fun x x_1 => x +ᵥ x_1) a) g
                                                                                  @[simp]
                                                                                  theorem Filter.pure_smul {α : Type u_2} {β : Type u_3} [SMul α β] {g : Filter β} {a : α} :
                                                                                  pure a g = Filter.map ((fun x x_1 => x x_1) a) g
                                                                                  @[simp]
                                                                                  theorem Filter.vadd_pure {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {b : β} :
                                                                                  f +ᵥ pure b = Filter.map (fun x => x +ᵥ b) f
                                                                                  @[simp]
                                                                                  theorem Filter.smul_pure {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {b : β} :
                                                                                  f pure b = Filter.map (fun x => x b) f
                                                                                  theorem Filter.pure_vadd_pure {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} {b : β} :
                                                                                  pure a +ᵥ pure b = pure (a +ᵥ b)
                                                                                  theorem Filter.pure_smul_pure {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} {b : β} :
                                                                                  pure a pure b = pure (a b)
                                                                                  theorem Filter.vadd_le_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f₁ : Filter α} {f₂ : Filter α} {g₁ : Filter β} {g₂ : Filter β} :
                                                                                  f₁ f₂g₁ g₂f₁ +ᵥ g₁ f₂ +ᵥ g₂
                                                                                  theorem Filter.smul_le_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f₁ : Filter α} {f₂ : Filter α} {g₁ : Filter β} {g₂ : Filter β} :
                                                                                  f₁ f₂g₁ g₂f₁ g₁ f₂ g₂
                                                                                  theorem Filter.vadd_le_vadd_left {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g₁ : Filter β} {g₂ : Filter β} :
                                                                                  g₁ g₂f +ᵥ g₁ f +ᵥ g₂
                                                                                  theorem Filter.smul_le_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g₁ : Filter β} {g₂ : Filter β} :
                                                                                  g₁ g₂f g₁ f g₂
                                                                                  theorem Filter.vadd_le_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {f₁ : Filter α} {f₂ : Filter α} {g : Filter β} :
                                                                                  f₁ f₂f₁ +ᵥ g f₂ +ᵥ g
                                                                                  theorem Filter.smul_le_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {f₁ : Filter α} {f₂ : Filter α} {g : Filter β} :
                                                                                  f₁ f₂f₁ g f₂ g
                                                                                  @[simp]
                                                                                  theorem Filter.le_vadd_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter α} {g : Filter β} {h : Filter β} :
                                                                                  h f +ᵥ g ∀ ⦃s : Set α⦄, s f∀ ⦃t : Set β⦄, t gs +ᵥ t h
                                                                                  @[simp]
                                                                                  theorem Filter.le_smul_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter α} {g : Filter β} {h : Filter β} :
                                                                                  h f g ∀ ⦃s : Set α⦄, s f∀ ⦃t : Set β⦄, t gs t h
                                                                                  instance Filter.covariant_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] :
                                                                                  CovariantClass (Filter α) (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x x_1
                                                                                  Equations
                                                                                  theorem Filter.covariant_vadd.proof_1 {α : Type u_1} {β : Type u_2} [VAdd α β] :
                                                                                  CovariantClass (Filter α) (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x x_1
                                                                                  instance Filter.covariant_smul {α : Type u_2} {β : Type u_3} [SMul α β] :
                                                                                  CovariantClass (Filter α) (Filter β) (fun x x_1 => x x_1) fun x x_1 => x x_1
                                                                                  Equations

                                                                                  Scalar subtraction of filters #

                                                                                  def Filter.instVSub {α : Type u_2} {β : Type u_3} [VSub α β] :
                                                                                  VSub (Filter α) (Filter β)

                                                                                  The filter f -ᵥ g is generated by {s -ᵥ t | s ∈ f, t ∈ g} in locale Pointwise.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem Filter.map₂_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {g : Filter β} :
                                                                                    Filter.map₂ (fun x x_1 => x -ᵥ x_1) f g = f -ᵥ g
                                                                                    theorem Filter.mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {g : Filter β} {s : Set α} :
                                                                                    s f -ᵥ g t₁ t₂, t₁ f t₂ g t₁ -ᵥ t₂ s
                                                                                    theorem Filter.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {g : Filter β} {s : Set β} {t : Set β} :
                                                                                    s ft gs -ᵥ t f -ᵥ g
                                                                                    @[simp]
                                                                                    theorem Filter.bot_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {g : Filter β} :
                                                                                    @[simp]
                                                                                    theorem Filter.vsub_bot {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} :
                                                                                    @[simp]
                                                                                    theorem Filter.vsub_eq_bot_iff {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {g : Filter β} :
                                                                                    f -ᵥ g = f = g =
                                                                                    @[simp]
                                                                                    theorem Filter.vsub_neBot_iff {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {g : Filter β} :
                                                                                    theorem Filter.NeBot.vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {g : Filter β} :
                                                                                    theorem Filter.NeBot.of_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {g : Filter β} :
                                                                                    theorem Filter.NeBot.of_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {g : Filter β} :
                                                                                    @[simp]
                                                                                    theorem Filter.pure_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {g : Filter β} {a : β} :
                                                                                    pure a -ᵥ g = Filter.map ((fun x x_1 => x -ᵥ x_1) a) g
                                                                                    @[simp]
                                                                                    theorem Filter.vsub_pure {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {b : β} :
                                                                                    f -ᵥ pure b = Filter.map (fun x => x -ᵥ b) f
                                                                                    theorem Filter.pure_vsub_pure {α : Type u_2} {β : Type u_3} [VSub α β] {a : β} {b : β} :
                                                                                    pure a -ᵥ pure b = pure (a -ᵥ b)
                                                                                    theorem Filter.vsub_le_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {f₁ : Filter β} {f₂ : Filter β} {g₁ : Filter β} {g₂ : Filter β} :
                                                                                    f₁ f₂g₁ g₂f₁ -ᵥ g₁ f₂ -ᵥ g₂
                                                                                    theorem Filter.vsub_le_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {g₁ : Filter β} {g₂ : Filter β} :
                                                                                    g₁ g₂f -ᵥ g₁ f -ᵥ g₂
                                                                                    theorem Filter.vsub_le_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {f₁ : Filter β} {f₂ : Filter β} {g : Filter β} :
                                                                                    f₁ f₂f₁ -ᵥ g f₂ -ᵥ g
                                                                                    @[simp]
                                                                                    theorem Filter.le_vsub_iff {α : Type u_2} {β : Type u_3} [VSub α β] {f : Filter β} {g : Filter β} {h : Filter α} :
                                                                                    h f -ᵥ g ∀ ⦃s : Set β⦄, s f∀ ⦃t : Set β⦄, t gs -ᵥ t h

                                                                                    Translation/scaling of filters #

                                                                                    def Filter.instVAddFilter {α : Type u_2} {β : Type u_3} [VAdd α β] :
                                                                                    VAdd α (Filter β)

                                                                                    a +ᵥ f is the map of f under a +ᵥ in locale Pointwise.

                                                                                    Equations
                                                                                    • Filter.instVAddFilter = { vadd := fun a => Filter.map ((fun x x_1 => x +ᵥ x_1) a) }
                                                                                    Instances For
                                                                                      def Filter.instSMulFilter {α : Type u_2} {β : Type u_3} [SMul α β] :
                                                                                      SMul α (Filter β)

                                                                                      a • f is the map of f under a • in locale Pointwise.

                                                                                      Equations
                                                                                      • Filter.instSMulFilter = { smul := fun a => Filter.map ((fun x x_1 => x x_1) a) }
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem Filter.map_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} :
                                                                                        Filter.map (fun b => a +ᵥ b) f = a +ᵥ f
                                                                                        @[simp]
                                                                                        theorem Filter.map_smul {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} :
                                                                                        Filter.map (fun b => a b) f = a f
                                                                                        theorem Filter.mem_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {s : Set β} {a : α} :
                                                                                        s a +ᵥ f (fun x x_1 => x +ᵥ x_1) a ⁻¹' s f
                                                                                        theorem Filter.mem_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {s : Set β} {a : α} :
                                                                                        s a f (fun x x_1 => x x_1) a ⁻¹' s f
                                                                                        theorem Filter.vadd_set_mem_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {s : Set β} {a : α} :
                                                                                        s fa +ᵥ s a +ᵥ f
                                                                                        theorem Filter.smul_set_mem_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {s : Set β} {a : α} :
                                                                                        s fa s a f
                                                                                        @[simp]
                                                                                        theorem Filter.vadd_filter_bot {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} :
                                                                                        @[simp]
                                                                                        theorem Filter.smul_filter_bot {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} :
                                                                                        @[simp]
                                                                                        theorem Filter.vadd_filter_eq_bot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} :
                                                                                        a +ᵥ f = f =
                                                                                        @[simp]
                                                                                        theorem Filter.smul_filter_eq_bot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} :
                                                                                        a f = f =
                                                                                        @[simp]
                                                                                        theorem Filter.vadd_filter_neBot_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} :
                                                                                        @[simp]
                                                                                        theorem Filter.smul_filter_neBot_iff {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} :
                                                                                        theorem Filter.NeBot.vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} :
                                                                                        theorem Filter.NeBot.smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} :
                                                                                        theorem Filter.NeBot.of_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} :
                                                                                        theorem Filter.NeBot.of_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} :
                                                                                        theorem Filter.vadd_filter_le_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] {f₁ : Filter β} {f₂ : Filter β} {a : α} (hf : f₁ f₂) :
                                                                                        a +ᵥ f₁ a +ᵥ f₂
                                                                                        theorem Filter.smul_filter_le_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] {f₁ : Filter β} {f₂ : Filter β} {a : α} (hf : f₁ f₂) :
                                                                                        a f₁ a f₂
                                                                                        theorem Filter.covariant_vadd_filter.proof_1 {α : Type u_1} {β : Type u_2} [VAdd α β] :
                                                                                        CovariantClass α (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x x_1
                                                                                        instance Filter.covariant_vadd_filter {α : Type u_2} {β : Type u_3} [VAdd α β] :
                                                                                        CovariantClass α (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x x_1
                                                                                        Equations
                                                                                        instance Filter.covariant_smul_filter {α : Type u_2} {β : Type u_3} [SMul α β] :
                                                                                        CovariantClass α (Filter β) (fun x x_1 => x x_1) fun x x_1 => x x_1
                                                                                        Equations
                                                                                        instance Filter.vaddCommClass_filter {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
                                                                                        Equations
                                                                                        theorem Filter.vaddCommClass_filter.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
                                                                                        instance Filter.smulCommClass_filter {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
                                                                                        Equations
                                                                                        theorem Filter.vaddCommClass_filter'.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
                                                                                        theorem Filter.vaddCommClass_filter''.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
                                                                                        theorem Filter.vaddCommClass.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
                                                                                        instance Filter.vaddCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
                                                                                        Equations
                                                                                        instance Filter.smulCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
                                                                                        Equations
                                                                                        instance Filter.vaddAssocClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
                                                                                        Equations
                                                                                        theorem Filter.vaddAssocClass.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
                                                                                        instance Filter.isScalarTower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
                                                                                        Equations
                                                                                        theorem Filter.vaddAssocClass'.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
                                                                                        instance Filter.vaddAssocClass' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
                                                                                        Equations
                                                                                        instance Filter.isScalarTower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
                                                                                        Equations
                                                                                        instance Filter.vaddAssocClass'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
                                                                                        Equations
                                                                                        theorem Filter.vaddAssocClass''.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] :
                                                                                        instance Filter.isScalarTower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
                                                                                        Equations
                                                                                        theorem Filter.isCentralVAdd.proof_1 {α : Type u_1} {β : Type u_2} [VAdd α β] [VAdd αᵃᵒᵖ β] [IsCentralVAdd α β] :
                                                                                        def Filter.addAction {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddAction α β] :

                                                                                        An additive action of an additive monoid α on a type β gives an additive action of Filter α on Filter β

                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          theorem Filter.addAction.proof_1 {α : Type u_2} {β : Type u_1} [AddMonoid α] [AddAction α β] (f : Filter β) :
                                                                                          Filter.map₂ (fun x x_1 => x +ᵥ x_1) (pure 0) f = f
                                                                                          theorem Filter.addAction.proof_2 {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddAction α β] (f : Filter α) (g : Filter α) (h : Filter β) :
                                                                                          Filter.map₂ (fun x x_1 => x +ᵥ x_1) (Filter.map₂ (fun x x_1 => x + x_1) f g) h = Filter.map₂ (fun x x_1 => x +ᵥ x_1) f (Filter.map₂ (fun x x_1 => x +ᵥ x_1) g h)
                                                                                          def Filter.mulAction {α : Type u_2} {β : Type u_3} [Monoid α] [MulAction α β] :

                                                                                          A multiplicative action of a monoid α on a type β gives a multiplicative action of Filter α on Filter β.

                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            theorem Filter.addActionFilter.proof_1 {α : Type u_2} {β : Type u_1} [AddMonoid α] [AddAction α β] (f : Filter β) :
                                                                                            Filter.map (fun x => 0 +ᵥ x) f = f
                                                                                            def Filter.addActionFilter {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddAction α β] :

                                                                                            An additive action of an additive monoid on a type β gives an additive action on Filter β.

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              theorem Filter.addActionFilter.proof_2 {α : Type u_2} {β : Type u_1} [AddMonoid α] [AddAction α β] (a : α) (b : α) (f : Filter β) :
                                                                                              Filter.map (fun b => a + b +ᵥ b) f = Filter.map (fun b => a +ᵥ b) (Filter.map (fun b => b +ᵥ b) f)
                                                                                              def Filter.mulActionFilter {α : Type u_2} {β : Type u_3} [Monoid α] [MulAction α β] :

                                                                                              A multiplicative action of a monoid on a type β gives a multiplicative action on Filter β.

                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For
                                                                                                def Filter.distribMulActionFilter {α : Type u_2} {β : Type u_3} [Monoid α] [AddMonoid β] [DistribMulAction α β] :

                                                                                                A distributive multiplicative action of a monoid on an additive monoid β gives a distributive multiplicative action on Filter β.

                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For

                                                                                                  A multiplicative action of a monoid on a monoid β gives a multiplicative action on Set β.

                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For

                                                                                                    Note that we have neither SMulWithZero α (Filter β) nor SMulWithZero (Filter α) (Filter β) because 0 * ⊥ ≠ 0.

                                                                                                    theorem Filter.NeBot.smul_zero_nonneg {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {f : Filter α} (hf : Filter.NeBot f) :
                                                                                                    0 f 0
                                                                                                    theorem Filter.NeBot.zero_smul_nonneg {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {g : Filter β} (hg : Filter.NeBot g) :
                                                                                                    0 0 g
                                                                                                    theorem Filter.zero_smul_filter_nonpos {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {g : Filter β} :
                                                                                                    0 g 0
                                                                                                    theorem Filter.zero_smul_filter {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {g : Filter β} (hg : Filter.NeBot g) :
                                                                                                    0 g = 0