LeanPool.DirectedTopologyLean4.UnitIntervalAux

theorem unitIAux.zero_le (T : ↑unitInterval) : ⟨0, unitInterval.zero_mem⟩ ≤ T

theorem unitIAux.le_one (T : ↑unitInterval) : T ≤ ⟨1, unitInterval.one_mem⟩

theorem unitIAux.double_pos_of_pos {T : ↑unitInterval} (hT₀ : 0 < T) : 0 < 2 * ↑T

theorem unitIAux.double_sigma_pos_of_lt_one {T : ↑unitInterval} (hT₁ : T < 1) : 0 < 2 * (1 - ↑T)

theorem unitIAux.double_mem_I {t : ↑unitInterval} (ht : ↑t ≤ 2⁻¹) : 2 * ↑t ∈ unitInterval

theorem unitIAux.double_sub_one_mem_I {t : ↑unitInterval} (ht : 2⁻¹ ≤ ↑t) : 2 * ↑t - 1 ∈ unitInterval

theorem unitIAux.interp_left_le_of_le (T : ↑unitInterval) {a b : ↑unitInterval} (hab : a ≤ b) : ↑(unitInterval.symm T) * ↑a + ↑T ≤ ↑(unitInterval.symm T) * ↑b + ↑T

theorem unitIAux.half_mem_I : 2⁻¹ ∈ unitInterval

@[reducible, inline]

noncomputable abbrev unitIAux.halfI : ↑unitInterval

The midpoint 1/2 of the unit interval.

Equations

• unitIAux.halfI = ⟨2⁻¹, unitIAux.half_mem_I⟩

theorem unitIAux.has_T_half {t₀ t₁ : ↑unitInterval} (γ : Path t₀ t₁) (ht₀ : ↑t₀ < 2⁻¹) (ht₁ : ↑t₁ > 2⁻¹) : ∃ (T : ↑unitInterval), 0 < T ∧ T < 1 ∧ γ T = halfI