LeanPool.DirectedTopologyLean4.Fraction

@[reducible]

noncomputable def Fraction {i n : ℕ} (hn : 0 < n) (hi : i ≤ n) : ↑unitInterval

For any natural numbers i n : ℕ such that n is positive and i ≤ n, we have that the fraction i/n : ℝ lives in the unit interval

Equations

• Fraction hn hi = ⟨↑i / ↑n, ⋯⟩

@[reducible]

noncomputable def Fraction.ofPos {n : ℕ} (hn : 0 < n) : ↑unitInterval

For any positive number n : ℕ, we have the fraction 1/n : ℝ in the unit interval

Equations

• Fraction.ofPos hn = Fraction hn ⋯

@[simp]

theorem Fraction.Fraction_coe {i n : ℕ} (hn : 0 < n) (hi : i ≤ n) : ↑(Fraction hn hi) = ↑i / ↑n

theorem Fraction.ofPos_coe {n : ℕ} (hn : 0 < n) : ↑(ofPos hn) = 1 / ↑n

theorem Fraction.eq_zero {n : ℕ} (n_pos : 0 < n) : Fraction n_pos ⋯ = 0

For any postive n : ℕ, we have that 0/n = n.

theorem Fraction.eq_one {n : ℕ} (n_pos : 0 < n) : Fraction n_pos ⋯ = 1

For any postive n : ℕ, we have that n/n = n.

theorem Fraction.mul_inv {i n : ℕ} (i_pos : 0 < i) (hi_n : i ≤ n) : Fraction ⋯ hi_n * ofPos i_pos = ofPos ⋯

For any i n : ℕ with 0 < i ≤ n, we have that i/n * 1/i = 1/n as members of I.

theorem Fraction.pos_of_pos {n i : ℕ} (hi : 0 < i) (hn : i ≤ n) : 0 < Fraction ⋯ hn

For any n i : ℕ with 0 < i ≤ n, we have that 0 < i/n.

theorem Fraction.lt_one_of_lt {n i : ℕ} (hi : 0 ≤ i) (hn : i < n) : Fraction ⋯ ⋯ < 1

For any n i : ℕ with 0 ≤ i < n, we have that i/n < 1.

theorem Fraction.ofPos_pos {n : ℕ} (hn : 0 < n) : 0 < ofPos hn

theorem Fraction.ofPos_lt_one {n : ℕ} (hn : 1 < n) : ofPos ⋯ < 1

theorem Fraction.lt_frac_succ {n m : ℕ} (hn : m < n) : Fraction ⋯ ⋯ < Fraction ⋯ ⋯