LeanPool.DirectedTopologyLean4.PathCover

def Dipath.covered {X : dTopCat} {X₀ X₁ : Set ↑X} {x₀ x₁ : ↑X} (hX : X₀ ∪ X₁ = Set.univ) (γ : Dipath x₀ x₁) : Prop

A dipath γ is covered by the cover X₀ ∪ X₁ = univ when its range lies inside one of the two sets.

Equations

• Dipath.covered hX γ = (Set.range ⇑γ ⊆ X₀ ∨ Set.range ⇑γ ⊆ X₁)

theorem Dipath.covered.covered_refl {X : dTopCat} {X₀ X₁ : Set ↑X} (x : ↑X) (hX : X₀ ∪ X₁ = Set.univ) : covered hX (refl x)

theorem Dipath.covered.covered_of_extended_image_subset {X : dTopCat} {X₀ X₁ : Set ↑X} {x₀ x₁ : ↑X} (γ : Dipath x₀ x₁) (hX : X₀ ∪ X₁ = Set.univ) (hγ : ⇑γ.extend '' unitInterval ⊆ X₀ ∨ ⇑γ.extend '' unitInterval ⊆ X₁) : covered hX γ

theorem Dipath.covered.covered_of_covered_trans {X : dTopCat} {X₀ X₁ : Set ↑X} {x₀ x₁ x₂ : ↑X} {γ₁ : Dipath x₀ x₁} {γ₂ : Dipath x₁ x₂} {hX : X₀ ∪ X₁ = Set.univ} (hγ : covered hX (γ₁.trans γ₂)) : covered hX γ₁ ∧ covered hX γ₂

theorem Dipath.covered.covered_subparam_of_covered {X : dTopCat} {X₀ X₁ : Set ↑X} {x₀ x₁ : ↑X} {γ : Dipath x₀ x₁} {hX : X₀ ∪ X₁ = Set.univ} (hγ : covered hX γ) (f : D(↑unitInterval,↑unitInterval)) : covered hX (γ.subparam f)

theorem Dipath.covered.covered_reparam_iff {X : dTopCat} {X₀ X₁ : Set ↑X} {x₀ x₁ : ↑X} (γ : Dipath x₀ x₁) (hX : X₀ ∪ X₁ = Set.univ) (f : D(↑unitInterval,↑unitInterval)) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : covered hX γ ↔ covered hX (γ.reparam f hf₀ hf₁)

theorem Dipath.covered.covered_cast_iff {X : dTopCat} {X₀ X₁ : Set ↑X} {x₀ x₁ x₀' x₁' : ↑X} (γ : Dipath x₀ x₁) (hX : X₀ ∪ X₁ = Set.univ) (hx₀ : x₀' = x₀) (hx₁ : x₁' = x₁) : covered hX γ ↔ covered hX (γ.cast hx₀ hx₁)

theorem Dipath.covered.covered_split_path {X : dTopCat} {X₀ X₁ : Set ↑X} {x₀ x₁ : ↑X} {γ : Dipath x₀ x₁} {hX : X₀ ∪ X₁ = Set.univ} {T : ↑unitInterval} (hT₀ : 0 < T) (hT₁ : T < 1) (hγ : covered hX γ) : covered hX (SplitDipath.FirstPart γ T) ∧ covered hX (SplitDipath.SecondPart γ T)

If γ is a dipath that is covered, then by splitting it into two parts [0, T] and [T, 1], both parts remain covered

def Dipath.coveredPartwise {X : dTopCat} {X₀ X₁ : Set ↑X} (hX : X₀ ∪ X₁ = Set.univ) {x y : ↑X} (γ : Dipath x y) (n : ℕ) : Prop

We say that coveredPartwise hX γ n if a dipath γ can be split into n+1 parts, each of which is covered by X₁ or X₂

Equations

• Dipath.coveredPartwise hX γ Nat.zero = Dipath.covered hX γ
• Dipath.coveredPartwise hX γ n_2.succ = (Dipath.covered hX (SplitDipath.FirstPart γ (Fraction.ofPos ⋯)) ∧ Dipath.coveredPartwise hX (SplitDipath.SecondPart γ (Fraction.ofPos ⋯)) n_2)

theorem Dipath.coveredPartwise.covered_partwise_of_equal {X : dTopCat} {X₀ X₁ : Set ↑X} (hX : X₀ ∪ X₁ = Set.univ) {x₀ x₁ : ↑X} {γ₁ γ₂ : Dipath x₀ x₁} {n m : ℕ} (h : γ₁ = γ₂) (h' : n = m) (hγ₁ : coveredPartwise hX γ₁ n) : coveredPartwise hX γ₂ m

theorem Dipath.coveredPartwise.covered_partwise_of_covered {X : dTopCat} {X₀ X₁ : Set ↑X} {hX : X₀ ∪ X₁ = Set.univ} (n : ℕ) {x₀ x₁ : ↑X} {γ : Dipath x₀ x₁} : covered hX γ → coveredPartwise hX γ n

If γ is a dipath that is fully covered, then it is also partwise covered for all n ∈ ℕ

theorem Dipath.coveredPartwise.covered_partwise_cast_iff {X : dTopCat} {X₀ X₁ : Set ↑X} (hX : X₀ ∪ X₁ = Set.univ) {n : ℕ} {x₀ x₁ x₀' x₁' : ↑X} (γ : Dipath x₀ x₁) (hx₀ : x₀' = x₀) (hx₁ : x₁' = x₁) : coveredPartwise hX γ n ↔ coveredPartwise hX (γ.cast hx₀ hx₁) n

theorem Dipath.coveredPartwise.covered_partwise_of_covered_by_intervals {X : dTopCat} {X₀ X₁ : Set ↑X} {hX : X₀ ∪ X₁ = Set.univ} (n : ℕ) {x₀ x₁ : ↑X} {γ : Dipath x₀ x₁} : (∀ i < n + 1, ⇑γ.extend '' Set.Icc (↑i / (↑n + 1)) ((↑i + 1) / (↑n + 1)) ⊆ X₀ ∨ ⇑γ.extend '' Set.Icc (↑i / (↑n + 1)) ((↑i + 1) / (↑n + 1)) ⊆ X₁) → coveredPartwise hX γ n

A dipath γ that can be covered with n+1 intervals can satisfied coveredPartwise _ γ n. This is the converse of covered_by_intervals_of_covered_partwise.

theorem Dipath.coveredPartwise.covered_by_intervals_of_covered_partwise {X : dTopCat} {X₀ X₁ : Set ↑X} {hX : X₀ ∪ X₁ = Set.univ} (n : ℕ) {x₀ x₁ : ↑X} {γ : Dipath x₀ x₁} : coveredPartwise hX γ n → ∀ i < n + 1, ⇑γ.extend '' Set.Icc (↑i / (↑n + 1)) ((↑i + 1) / (↑n + 1)) ⊆ X₀ ∨ ⇑γ.extend '' Set.Icc (↑i / (↑n + 1)) ((↑i + 1) / (↑n + 1)) ⊆ X₁

A dipath γ that satisfies coveredPartwise _ γ n can be covered with n+1 intervals. This is the converse of covered_partwise_of_covered_by_intervals.

theorem Dipath.coveredPartwise.covered_partwise_first_part_d {X : dTopCat} {X₀ X₁ : Set ↑X} (hX : X₀ ∪ X₁ = Set.univ) {n d : ℕ} (hd_n : d.succ < n.succ) {x₀ x₁ : ↑X} {γ : Dipath x₀ x₁} : coveredPartwise hX γ n → coveredPartwise hX (SplitDipath.FirstPart γ (Fraction ⋯ ⋯)) d

Let γ be a dipath covered by n+1 parts. Let 0 < k < n+1 be given. Then the first part of γ, split by k/(n+1) is covered by k parts. Here, k = d.succ, so we don't need the requirement k > 0.

theorem Dipath.coveredPartwise.covered_partwise_second_part_d {X : dTopCat} {X₀ X₁ : Set ↑X} (hX : X₀ ∪ X₁ = Set.univ) {n d : ℕ} (hd_n : d.succ < n.succ) {x₀ x₁ : ↑X} {γ : Dipath x₀ x₁} : coveredPartwise hX γ n → coveredPartwise hX (SplitDipath.SecondPart γ (Fraction ⋯ ⋯)) (n - d.succ)

Input: (d+1) < (n+1) --> split at (d+1)/(n+1) Let γ be a dipath covered by n+1 parts. Let 0 < k < n+1 be given. Then the second part of γ, split by k/(n+1) is covered by n+1-k parts. Here, k = d.succ, so we don't need the requirement k > 0.

theorem Dipath.coveredPartwise.covered_partwise_first_part_end_split {X : dTopCat} {X₀ X₁ : Set ↑X} (hX : X₀ ∪ X₁ = Set.univ) {n : ℕ} {x₀ x₁ : ↑X} {γ : Dipath x₀ x₁} (hγ : coveredPartwise hX γ n.succ) : coveredPartwise hX (SplitDipath.FirstPart γ (Fraction ⋯ ⋯)) n

Let γ be a dipath covered by n+2 parts. Then the first part of γ, split by (n+1)/(n+2) is covered by n+1 parts.

theorem Dipath.coveredPartwise.covered_second_part_end_split {X : dTopCat} {X₀ X₁ : Set ↑X} (hX : X₀ ∪ X₁ = Set.univ) {n : ℕ} {x₀ x₁ : ↑X} {γ : Dipath x₀ x₁} (hγ : coveredPartwise hX γ n.succ) : covered hX (SplitDipath.SecondPart γ (Fraction ⋯ ⋯))

Let γ be a dipath covered by n+2 parts. Then the second part of γ, split by (n+1)/(n+2) is covered

theorem Dipath.coveredPartwise.covered_partwise_of_parts {X : dTopCat} {X₀ X₁ : Set ↑X} (hX : X₀ ∪ X₁ = Set.univ) {n : ℕ} (hn : 0 < n) {k : ℕ} (hk : k > 0) {x₀ x₁ : ↑X} {γ : Dipath x₀ x₁} : coveredPartwise hX (SplitDipath.FirstPart γ (Fraction.ofPos ⋯)) (k - 1) ∧ coveredPartwise hX (SplitDipath.SecondPart γ (Fraction.ofPos ⋯)) (n * k - 1) → coveredPartwise hX γ ((n + 1) * k - 1)

Let γ be a dipath and n ≥ 2: If the first part [0, 1/(n+1)] can be covered with k intervals and the second part [1/(n+1), 1] can be covered with kn intervals, then the entire path can be covered with k(n+1) intervals.

theorem Dipath.coveredPartwise.covered_partwise_refine {X : dTopCat} {X₀ X₁ : Set ↑X} (hX : X₀ ∪ X₁ = Set.univ) (n k : ℕ) {x₀ x₁ : ↑X} {γ : Dipath x₀ x₁} : coveredPartwise hX γ n → coveredPartwise hX γ ((n + 1) * (k + 1) - 1)

If a dipath γ can be covered in n+1 parts, it can also be covered in (k+1) * (n+1) parts

theorem Dipath.coveredPartwise.covered_partwise_trans {X : dTopCat} {X₀ X₁ : Set ↑X} {hX : X₀ ∪ X₁ = Set.univ} {n : ℕ} {x₀ x₁ x₂ : ↑X} {γ₁ : Dipath x₀ x₁} {γ₂ : Dipath x₁ x₂} (hγ₁ : coveredPartwise hX γ₁ n) (hγ₂ : coveredPartwise hX γ₂ n) : coveredPartwise hX (γ₁.trans γ₂) (n + n).succ

theorem Dipath.coveredPartwise.has_interval_division {X : dTopCat} {x₀ x₁ : ↑X} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) (γ : Dipath x₀ x₁) : ∃ n > 0, ∀ i < n, Set.Icc (↑i / ↑n) ((↑i + 1) / ↑n) ⊆ ⇑γ.extend ⁻¹' X₁ ∨ Set.Icc (↑i / ↑n) ((↑i + 1) / ↑n) ⊆ ⇑γ.extend ⁻¹' X₂

theorem Dipath.coveredPartwise.has_subpaths {X : dTopCat} {x₀ x₁ : ↑X} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) (γ : Dipath x₀ x₁) : ∃ (n : ℕ), coveredPartwise hX γ n

If γ is a dipath and a directed space X is covered by two opens X₁ and X₂, then γ is n-covered for some n.