# 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 #

• [nLab, Coalgebra of the real interval] (https://ncatlab.org/nlab/show/coalgebra+of+the+real+interval)
theorem TwoPointing.ext_iff {α : Type u_1} (x : ) (y : ) :
x = y x.toProd.fst = y.toProd.fst x.toProd.snd = y.toProd.snd
theorem TwoPointing.ext {α : Type u_1} (x : ) (y : ) (fst : x.toProd.fst = y.toProd.fst) (snd : x.toProd.snd = y.toProd.snd) :
x = y
structure TwoPointing (α : Type u_1) extends :
Type u_1
• fst and snd are distinct terms

fst_ne_snd : toProd.fst toProd.snd

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

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

Swaps the two pointed elements.

Equations
• = { toProd := (p.toProd.snd, p.toProd.fst), fst_ne_snd := (_ : p.toProd.snd p.toProd.fst) }
theorem TwoPointing.swap_fst {α : Type u_1} (p : ) :
().toProd.fst = p.toProd.snd
theorem TwoPointing.swap_snd {α : Type u_1} (p : ) :
().toProd.snd = p.toProd.fst
@[simp]
theorem TwoPointing.swap_swap {α : Type u_1} (p : ) :
theorem TwoPointing.to_nontrivial {α : Type u_1} (p : ) :
instance TwoPointing.instNonemptyTwoPointing {α : Type u_1} [inst : ] :
Equations
def TwoPointing.pi (α : Type u_1) {β : Type u_2} (q : ) [inst : ] :
TwoPointing (αβ)

The two-pointing of constant functions.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem TwoPointing.pi_fst (α : Type u_1) {β : Type u_2} (q : ) [inst : ] :
().toProd.fst = Function.const α q.toProd.fst
@[simp]
theorem TwoPointing.pi_snd (α : Type u_1) {β : Type u_2} (q : ) [inst : ] :
().toProd.snd = Function.const α q.toProd.snd
def TwoPointing.prod {α : Type u_1} {β : Type u_2} (p : ) (q : ) :
TwoPointing (α × β)

The product of two two-pointings.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem TwoPointing.prod_fst {α : Type u_1} {β : Type u_2} (p : ) (q : ) :
().toProd.fst = (p.toProd.fst, q.toProd.fst)
@[simp]
theorem TwoPointing.prod_snd {α : Type u_1} {β : Type u_2} (p : ) (q : ) :
().toProd.snd = (p.toProd.snd, q.toProd.snd)
def TwoPointing.sum {α : Type u_1} {β : Type u_2} (p : ) (q : ) :

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

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

The false, true two-pointing of Bool.

Equations

The False, True two-pointing of Prop.

Equations