Documentation

Mathlib.Data.TwoPointing

Two-pointings #

This file defines TwoPointing α, the type of two pointings of α. A two-pointing is the data of two distinct terms.

This is morally a Type-valued Nontrivial. Another type which is quite close in essence is Sym2. Categorically speaking, prod is a cospan in the category of types. This forms the category of bipointed types. Two-pointed types form a full subcategory of those.

References #

theorem TwoPointing.ext {α : Type u_3} {x : TwoPointing α} {y : TwoPointing α} (fst : x.fst = y.fst) (snd : x.snd = y.snd) :
x = y
theorem TwoPointing.ext_iff {α : Type u_3} {x : TwoPointing α} {y : TwoPointing α} :
x = y x.fst = y.fst x.snd = y.snd
structure TwoPointing (α : Type u_3) extends Prod :
Type u_3

Two-pointing of a type. This is a Type-valued termed Nontrivial.

  • fst : α
  • snd : α
  • fst_ne_snd : self.fst self.snd

    fst and snd are distinct terms

Instances For
    theorem TwoPointing.fst_ne_snd {α : Type u_3} (self : TwoPointing α) :
    self.fst self.snd

    fst and snd are distinct terms

    instance instDecidableEqTwoPointing :
    {α : Type u_3} → [inst : DecidableEq α] → DecidableEq (TwoPointing α)
    Equations
    • instDecidableEqTwoPointing = decEqTwoPointing✝
    theorem TwoPointing.snd_ne_fst {α : Type u_1} (p : TwoPointing α) :
    p.snd p.fst
    @[simp]
    theorem TwoPointing.swap_toProd {α : Type u_1} (p : TwoPointing α) :
    p.swap.toProd = (p.snd, p.fst)
    def TwoPointing.swap {α : Type u_1} (p : TwoPointing α) :

    Swaps the two pointed elements.

    Equations
    • p.swap = { toProd := (p.snd, p.fst), fst_ne_snd := }
    Instances For
      theorem TwoPointing.swap_fst {α : Type u_1} (p : TwoPointing α) :
      p.swap.fst = p.snd
      theorem TwoPointing.swap_snd {α : Type u_1} (p : TwoPointing α) :
      p.swap.snd = p.fst
      @[simp]
      theorem TwoPointing.swap_swap {α : Type u_1} (p : TwoPointing α) :
      p.swap.swap = p
      Equations
      • =
      def TwoPointing.pi (α : Type u_1) {β : Type u_2} (q : TwoPointing β) [Nonempty α] :
      TwoPointing (αβ)

      The two-pointing of constant functions.

      Equations
      • TwoPointing.pi α q = { toProd := (fun (x : α) => q.fst, fun (x : α) => q.snd), fst_ne_snd := }
      Instances For
        @[simp]
        theorem TwoPointing.pi_fst (α : Type u_1) {β : Type u_2} (q : TwoPointing β) [Nonempty α] :
        (TwoPointing.pi α q).fst = Function.const α q.fst
        @[simp]
        theorem TwoPointing.pi_snd (α : Type u_1) {β : Type u_2} (q : TwoPointing β) [Nonempty α] :
        (TwoPointing.pi α q).snd = Function.const α q.snd
        def TwoPointing.prod {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β) :
        TwoPointing (α × β)

        The product of two two-pointings.

        Equations
        • p.prod q = { toProd := ((p.fst, q.fst), p.snd, q.snd), fst_ne_snd := }
        Instances For
          @[simp]
          theorem TwoPointing.prod_fst {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β) :
          (p.prod q).fst = (p.fst, q.fst)
          @[simp]
          theorem TwoPointing.prod_snd {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β) :
          (p.prod q).snd = (p.snd, q.snd)
          def TwoPointing.sum {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β) :

          The sum of two pointings. Keeps the first point from the left and the second point from the right.

          Equations
          Instances For
            @[simp]
            theorem TwoPointing.sum_fst {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β) :
            (p.sum q).fst = Sum.inl p.fst
            @[simp]
            theorem TwoPointing.sum_snd {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β) :
            (p.sum q).snd = Sum.inr q.snd

            The false, true two-pointing of Bool.

            Equations
            Instances For

              The False, True two-pointing of Prop.

              Equations
              Instances For