def TwinPrime.IsTwinPrimeAt (p : ℕ) : Prop

p begins a twin-prime pair.

Equations

• TwinPrime.IsTwinPrimeAt p = (Nat.Prime p ∧ Nat.Prime (p + 2))

def TwinPrime.IsTwinPrimePair (p q : ℕ) : Prop

Explicit ordered pair form of a twin-prime witness.

Equations

• TwinPrime.IsTwinPrimePair p q = (Nat.Prime p ∧ Nat.Prime q ∧ q = p + 2)

def TwinPrime.HasTwinPrimeFrom (N : ℕ) : Prop

There is a twin-prime starter at least N.

Equations

• TwinPrime.HasTwinPrimeFrom N = ∃ (p : ℕ), N ≤ p ∧ TwinPrime.IsTwinPrimeAt p

def TwinPrime.HasTwinPrimeUpTo (N : ℕ) : Prop

There is a twin-prime starter at most N.

Equations

• TwinPrime.HasTwinPrimeUpTo N = ∃ (p : ℕ), p ≤ N ∧ TwinPrime.IsTwinPrimeAt p

instance TwinPrime.instDecidableIsTwinPrimeAt (p : ℕ) : Decidable (IsTwinPrimeAt p)

Equations

• TwinPrime.instDecidableIsTwinPrimeAt p = id inferInstance

instance TwinPrime.instDecidableIsTwinPrimePair (p q : ℕ) : Decidable (IsTwinPrimePair p q)

Equations

• TwinPrime.instDecidableIsTwinPrimePair p q = id inferInstance