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 : TwoPointing α) (y : TwoPointing α) :

x = y ↔ x.toProd.fst = y.toProd.fst ∧ x.toProd.snd = y.toProd.snd

theorem TwoPointing.ext {α : Type u_1} (x : TwoPointing α) (y : TwoPointing α) (fst : x.toProd.fst = y.toProd.fst) (snd : x.toProd.snd = y.toProd.snd) :

x = y

structure TwoPointing (α : Type u_1) extends Prod :

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 : DecidableEq α] → DecidableEq (TwoPointing α)

Equations

instDecidableEqTwoPointing = decEqTwoPointing✝

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

p.toProd.snd ≠ p.toProd.fst

@[simp]

theorem TwoPointing.swap_toProd {α : Type u_1} (p : TwoPointing α) :

(TwoPointing.swap p).toProd = (p.toProd.snd, p.toProd.fst)

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

Swaps the two pointed elements.

Equations

TwoPointing.swap p = { toProd := (p.toProd.snd, p.toProd.fst), fst_ne_snd := (_ : p.toProd.snd ≠ p.toProd.fst) }

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

(TwoPointing.swap p).toProd.fst = p.toProd.snd

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

(TwoPointing.swap p).toProd.snd = p.toProd.fst

@[simp]

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

TwoPointing.swap (TwoPointing.swap p) = p

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

instance TwoPointing.instNonemptyTwoPointing {α : Type u_1} [inst : Nontrivial α] :

Nonempty (TwoPointing α)

Equations

@TwoPointing.instNonemptyTwoPointing = @TwoPointing.instNonemptyTwoPointing.proof_1

@[simp]

theorem TwoPointing.nonempty_two_pointing_iff {α : Type u_1} :

Nonempty (TwoPointing α) ↔ Nontrivial α

def TwoPointing.pi (α : Type u_1) {β : Type u_2} (q : TwoPointing β) [inst : Nonempty α] :

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 : TwoPointing β) [inst : Nonempty α] :

(TwoPointing.pi α q).toProd.fst = Function.const α q.toProd.fst

@[simp]

theorem TwoPointing.pi_snd (α : Type u_1) {β : Type u_2} (q : TwoPointing β) [inst : Nonempty α] :

(TwoPointing.pi α q).toProd.snd = Function.const α q.toProd.snd

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

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 : TwoPointing α) (q : TwoPointing β) :

(TwoPointing.prod p q).toProd.fst = (p.toProd.fst, q.toProd.fst)

@[simp]

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

(TwoPointing.prod p q).toProd.snd = (p.toProd.snd, q.toProd.snd)

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

TwoPointing (α ⊕ β)

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

Equations

TwoPointing.sum p q = { toProd := (Sum.inl p.toProd.fst, Sum.inr q.toProd.snd), fst_ne_snd := (_ : Sum.inl p.toProd.fst ≠ Sum.inr q.toProd.snd) }

@[simp]

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

(TwoPointing.sum p q).toProd.fst = Sum.inl p.toProd.fst

@[simp]

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

(TwoPointing.sum p q).toProd.snd = Sum.inr q.toProd.snd

def TwoPointing.bool :

TwoPointing Bool

The false, true two-pointing of Bool.

Equations

TwoPointing.bool = { toProd := (false, true), fst_ne_snd := Bool.ff_ne_tt }

@[simp]

theorem TwoPointing.bool_fst :

TwoPointing.bool.toProd.fst = false

@[simp]

theorem TwoPointing.bool_snd :

TwoPointing.bool.toProd.snd = true

instance TwoPointing.instInhabitedTwoPointingBool :

Inhabited (TwoPointing Bool)

Equations

TwoPointing.instInhabitedTwoPointingBool = { default := TwoPointing.bool }

def TwoPointing.prop :

TwoPointing Prop

The False, True two-pointing of Prop.

Equations

TwoPointing.prop = { toProd := (False, True), fst_ne_snd := false_ne_true }

@[simp]

theorem TwoPointing.prop_fst :

TwoPointing.prop.toProd.fst = False

@[simp]

theorem TwoPointing.prop_snd :

TwoPointing.prop.toProd.snd = True