Documentation

LeanPool.DirectedTopologyLean4.CoverLemma

Auxiliary lemmas #

source
theorem mid_point_Icc {i n : ℕ} (hn : n > 0) :
(2 * ↑i + 1) / (2 * ↑n) ∈ Set.Icc (↑i / ↑n) ((↑i + 1) / ↑n)

For any two natural numbers i n : ℕ with n > 0, we have that (2i+1)/(2n) is contained in the interval [i/n, (i+1)/n].

source
theorem mid_point_I {i n : ℕ} (hi : i < n) :
(2 * ↑i + 1) / (2 * ↑n) ∈ unitInterval

For any two natural numbers i n : ℕ with i < n, we have that (2i+1)/(2n) is contained in unit interval

source
theorem UnitIntervalSub.mem_I_of_mem_interval {t : ℝ} {n i : ℕ} (hi : i < n.succ) (h : t ∈ Set.Icc (↑i / ↑n.succ) (↑(i + 1) / ↑n.succ)) :
t ∈ unitInterval
source
theorem UnitIntervalSub.mem_I_of_mem_interval_coed {t : ℝ} {n i : ℕ} (hi : i < n.succ) (h : t ∈ Set.Icc (↑i / (↑n + 1)) ((↑i + 1) / (↑n + 1))) :
t ∈ unitInterval

Covering lemma for the unit interval #

source
theorem lebesgue_number_lemma_unit_interval {ι : Sort u} {c : ι → Set ℝ} (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : unitInterval ⊆ ⋃ (i : ι), c i) :
∃ n > 0, ∀ i < n, ∃ (j : ι), Set.Icc (↑i / ↑n) ((↑i + 1) / ↑n) ⊆ c j

Covering lemma for the unit square #

source
def UnitSquare :
Set (↑unitInterval × ↑unitInterval)

The full unit square as a subset of I × I.

Equations
Instances For
    source
    theorem compact_unitSquare :
    IsCompact UnitSquare
    source
    def UnitSubrectangle {n m i j : ℕ} (hi : i < n.succ) (hj : j < m.succ) :
    Set (↑unitInterval × ↑unitInterval)

    For any four natural numbers n m i j : ℕ such that i < n + 1 and j < m + 1, we have the rectangle [i/(n+1), (i+1)/(n+1)] × [j/(m+1), (j+1)/(m+1)] in the unit square.

    Equations
    Instances For
      source
      theorem UnitSubrectangle.mem_unitSquare (t : ↑unitInterval × ↑unitInterval) :
      t ∈ UnitSubrectangle ⋯ ⋯
      source
      theorem UnitSubrectangle.mem_unitSubrectangle {t₀ t₁ : ℝ} {n m i j : ℕ} (hi : i < n.succ) (hj : j < m.succ) (ht₀ : t₀ ∈ Set.Icc (↑i / ↑n.succ) (↑(i + 1) / ↑n.succ)) (ht₁ : t₁ ∈ Set.Icc (↑j / ↑m.succ) (↑(j + 1) / ↑m.succ)) :
      (⟨t₀, ⋯⟩, ⟨t₁, ⋯⟩) ∈ UnitSubrectangle hi hj
      source
      theorem lebesgue_number_lemma_unitSquare {ι : Sort u} {c : ι → Set (↑unitInterval × ↑unitInterval)} (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : UnitSquare ⊆ ⋃ (i : ι), c i) :
      ∃ (n : ℕ), ∀ (i j : ℕ) (hi : i < n.succ) (hj : j < n.succ), ∃ (a : ι), UnitSubrectangle hi hj ⊆ c a