LeanPool.WhiteheadTheorem.Shapes.UnitInterval

Imported Lean Pool material for LeanPool.WhiteheadTheorem.Shapes.UnitInterval.

instance unitInterval.continuousMul : ContinuousMul ↑unitInterval

@[reducible, inline]

abbrev unitInterval.zeroOne : Set ℝ

zeroOne

Equations

• unitInterval.zeroOne = {0, 1}

@[implicit_reducible]

instance unitInterval.instOfNatElemRealZeroOneOfNatNat : OfNat (↑zeroOne) 0

Equations

• unitInterval.instOfNatElemRealZeroOneOfNatNat = { ofNat := ⟨0, unitInterval.instOfNatElemRealZeroOneOfNatNat._proof_1⟩ }

@[implicit_reducible]

instance unitInterval.instOfNatElemRealZeroOneOfNatNat_1 : OfNat (↑zeroOne) 1

Equations

• unitInterval.instOfNatElemRealZeroOneOfNatNat_1 = { ofNat := ⟨1, unitInterval.instOfNatElemRealZeroOneOfNatNat_1._proof_1⟩ }

theorem unitInterval.zeroOne.val_eq_zero_or_val_eq_one (t : ↑zeroOne) : ↑t = 0 ∨ ↑t = 1

theorem unitInterval.zeroOne.eq_zero_or_eq_one (t : ↑zeroOne) : t = 0 ∨ t = 1

@[reducible, inline]

abbrev unitInterval.zeroOneIncl : C(↑zeroOne, ↑unitInterval)

zeroOneIncl

Equations

• unitInterval.zeroOneIncl = { toFun := fun (x : ↑unitInterval.zeroOne) => match x with | ⟨x, hx⟩ => ⟨x, ⋯⟩, continuous_toFun := unitInterval.zeroOneIncl._proof_3 }