mathlib documentation

data.two_pointing

Two-pointings #

This file defines two_pointing α, 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 #

[Coalgebra of the real interval] [http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/coalgebra+of+the+real+interval]

@[protected, instance]

def two_pointing.decidable_eq (α : Type u_3) [a : decidable_eq α] :

decidable_eq (two_pointing α)

theorem two_pointing.ext {α : Type u_3} (x y : two_pointing α) (h : x.to_prod = y.to_prod) :

x = y

@[ext]

structure two_pointing (α : Type u_3) :

Type u_3

to_prod : α × α
fst_ne_snd : self.to_prod.fst ≠ self.to_prod.snd

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

theorem two_pointing.ext_iff {α : Type u_3} (x y : two_pointing α) :

x = y ↔ x.to_prod = y.to_prod

theorem two_pointing.snd_ne_fst {α : Type u_1} (p : two_pointing α) :

p.to_prod.snd ≠ p.to_prod.fst

@[simp]

theorem two_pointing.swap_to_prod {α : Type u_1} (p : two_pointing α) :

p.swap.to_prod = (p.to_prod.snd, p.to_prod.fst)

def two_pointing.swap {α : Type u_1} (p : two_pointing α) :

two_pointing α

Swaps the two pointed elements.

Equations

p.swap = {to_prod := (p.to_prod.snd, p.to_prod.fst), fst_ne_snd := _}

theorem two_pointing.swap_fst {α : Type u_1} (p : two_pointing α) :

p.swap.to_prod.fst = p.to_prod.snd

theorem two_pointing.swap_snd {α : Type u_1} (p : two_pointing α) :

p.swap.to_prod.snd = p.to_prod.fst

@[simp]

theorem two_pointing.swap_swap {α : Type u_1} (p : two_pointing α) :

p.swap.swap = p

theorem two_pointing.to_nontrivial {α : Type u_1} (p : two_pointing α) :

@[protected, instance]

def two_pointing.nonempty {α : Type u_1} [nontrivial α] :

nonempty (two_pointing α)

@[simp]

theorem two_pointing.nonempty_two_pointing_iff {α : Type u_1} :

nonempty (two_pointing α) ↔ nontrivial α

def two_pointing.pi (α : Type u_1) {β : Type u_2} (q : two_pointing β) [nonempty α] :

two_pointing (α → β)

The two-pointing of constant functions.

Equations

two_pointing.pi α q = {to_prod := (λ (_x : α), q.to_prod.fst, λ (_x : α), q.to_prod.snd), fst_ne_snd := _}

@[simp]

theorem two_pointing.pi_fst (α : Type u_1) {β : Type u_2} (q : two_pointing β) [nonempty α] :

(two_pointing.pi α q).to_prod.fst = function.const α q.to_prod.fst

@[simp]

theorem two_pointing.pi_snd (α : Type u_1) {β : Type u_2} (q : two_pointing β) [nonempty α] :

(two_pointing.pi α q).to_prod.snd = function.const α q.to_prod.snd

def two_pointing.prod {α : Type u_1} {β : Type u_2} (p : two_pointing α) (q : two_pointing β) :

two_pointing (α × β)

The product of two two-pointings.

Equations

p.prod q = {to_prod := ((p.to_prod.fst, q.to_prod.fst), p.to_prod.snd, q.to_prod.snd), fst_ne_snd := _}

@[simp]

theorem two_pointing.prod_fst {α : Type u_1} {β : Type u_2} (p : two_pointing α) (q : two_pointing β) :

(p.prod q).to_prod.fst = (p.to_prod.fst, q.to_prod.fst)

@[simp]

theorem two_pointing.prod_snd {α : Type u_1} {β : Type u_2} (p : two_pointing α) (q : two_pointing β) :

(p.prod q).to_prod.snd = (p.to_prod.snd, q.to_prod.snd)

@[protected]

def two_pointing.sum {α : Type u_1} {β : Type u_2} (p : two_pointing α) (q : two_pointing β) :

two_pointing (α ⊕ β)

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

Equations

p.sum q = {to_prod := (sum.inl p.to_prod.fst, sum.inr q.to_prod.snd), fst_ne_snd := _}

@[simp]

theorem two_pointing.sum_fst {α : Type u_1} {β : Type u_2} (p : two_pointing α) (q : two_pointing β) :

(p.sum q).to_prod.fst = sum.inl p.to_prod.fst

@[simp]

theorem two_pointing.sum_snd {α : Type u_1} {β : Type u_2} (p : two_pointing α) (q : two_pointing β) :

(p.sum q).to_prod.snd = sum.inr q.to_prod.snd

@[protected]

def two_pointing.bool :

two_pointing bool

The ff, tt two-pointing of bool.

Equations

two_pointing.bool = {to_prod := (ff, tt), fst_ne_snd := bool.ff_ne_tt}

@[simp]

theorem two_pointing.bool_fst :

two_pointing.bool.to_prod.fst = ff

@[simp]

theorem two_pointing.bool_snd :

two_pointing.bool.to_prod.snd = tt

@[protected, instance]

def two_pointing.inhabited :

inhabited (two_pointing bool)

Equations

two_pointing.inhabited = {default := two_pointing.bool}

@[protected]

def two_pointing.Prop :

two_pointing Prop

The false, true two-pointing of Prop.

Equations

two_pointing.Prop = {to_prod := (false, true), fst_ne_snd := false_ne_true}

@[simp]

theorem two_pointing.Prop_fst :

two_pointing.Prop.to_prod.fst = false

@[simp]

theorem two_pointing.Prop_snd :

two_pointing.Prop.to_prod.snd = true