Documentation

ConNF.Mathlib.Pointwise

source
@[simp]
theorem Set.neg_sUnion {α : Type u_1} [InvolutiveNeg α] (S : Set (Set α)) :
-⋃₀ S = ⋃ s ∈ S, -s
source
@[simp]
theorem Set.inv_sUnion {α : Type u_1} [InvolutiveInv α] (S : Set (Set α)) :
(⋃₀ S)⁻¹ = ⋃ s ∈ S, s⁻¹
source
theorem Set.hasVaddNonempty.proof_1 {α : Type u_2} {β : Type u_1} [VAdd α β] (a : α) (s : { s : Set β // s.Nonempty }) :
(a +ᵥ ↑s).Nonempty
source
noncomputable def Set.hasVaddNonempty {α : Type u_1} {β : Type u_2} [VAdd α β] :
VAdd α { s : Set β // s.Nonempty }

The translation of nonempty set x +ᵥ s is defined as {x +ᵥ y | y ∈ s} in locale pointwise.

Equations
  • Set.hasVaddNonempty = { vadd := fun (a : α) (s : { s : Set β // s.Nonempty }) => ⟨a +ᵥ ↑s, ⋯⟩ }
Instances For
    source
    noncomputable def Set.hasSmulNonempty {α : Type u_1} {β : Type u_2} [SMul α β] :
    SMul α { s : Set β // s.Nonempty }

    The dilation of nonempty set x • s is defined as {x • y | y ∈ s} in locale pointwise.

    Equations
    • Set.hasSmulNonempty = { smul := fun (a : α) (s : { s : Set β // s.Nonempty }) => ⟨a • ↑s, ⋯⟩ }
    Instances For
      source
      @[simp]
      theorem Set.coe_vadd_nonempty {α : Type u_2} {β : Type u_1} [VAdd α β] (a : α) (s : { s : Set β // s.Nonempty }) :
      ↑(a +ᵥ s) = a +ᵥ ↑s
      source
      @[simp]
      theorem Set.coe_smul_nonempty {α : Type u_2} {β : Type u_1} [SMul α β] (a : α) (s : { s : Set β // s.Nonempty }) :
      ↑(a • s) = a • ↑s
      source
      @[simp]
      theorem Set.vadd_nonempty_mk {α : Type u_2} {β : Type u_1} [VAdd α β] (a : α) (s : Set β) (hs : s.Nonempty) :
      a +ᵥ ⟨s, hs⟩ = ⟨a +ᵥ s, ⋯⟩
      source
      @[simp]
      theorem Set.smul_nonempty_mk {α : Type u_2} {β : Type u_1} [SMul α β] (a : α) (s : Set β) (hs : s.Nonempty) :
      a • ⟨s, hs⟩ = ⟨a • s, ⋯⟩
      source
      theorem Set.addActionNonempty.proof_1 {β : Type u_1} :
      Function.Injective fun (a : { s : Set β // s.Nonempty }) => ↑a
      source
      noncomputable def Set.addActionNonempty {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddAction α β] :
      AddAction α { s : Set β // s.Nonempty }

      An additive action on a type gives an additive action on its nonempty sets.

      Equations
      Instances For
        source
        theorem Set.addActionNonempty.proof_2 {α : Type u_2} {β : Type u_1} [AddMonoid α] [AddAction α β] (a : α) (s : { s : Set β // s.Nonempty }) :
        ↑(a +ᵥ s) = a +ᵥ ↑s
        source
        noncomputable def Set.mulActionNonempty {α : Type u_1} {β : Type u_2} [Monoid α] [MulAction α β] :
        MulAction α { s : Set β // s.Nonempty }

        A multiplicative action on a type β gives a multiplicative action on its nonempty sets.

        Equations
        Instances For