Documentation

LeanPool.DirectedTopologyLean4.DirectedUnitInterval

LeanPool.DirectedTopologyLean4.DirectedUnitInterval #

source
@[implicit_reducible]
instance DirectedUnitInterval.instDirectedSpaceElemRealUnitInterval :
DirectedSpace ↑unitInterval

Construct the directed unit interval by using the preorder inherited from ℝ

Equations
source
def DirectedUnitInterval.IdentityPath :
Path 0 1

The identity on I as a path I → I.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem DirectedUnitInterval.isDipath_identityPath :
    IsDipath IdentityPath

    The identity path is a directed path.

    source
    theorem DirectedUnitInterval.isDipath_of_isDipath_comp_id {X : Type u} [DirectedSpace X] {x y : X} {γ : Path x y} (h : IsDipath (IdentityPath.map ⋯)) :
    IsDipath γ

    If γ is path and the identity path on I composed with γ is a directed path, then γ is a directed path.

    source
    theorem DirectedUnitInterval.monotone_of_directed (f : D(↑unitInterval,↑unitInterval)) :
    Monotone ⇑f

    A directed map from I to I is monotone

    source
    theorem DirectedUnitInterval.directed_of_monotone (f : C(↑unitInterval, ↑unitInterval)) (hf_mono : Monotone ⇑f) :
    DirectedMap.Directed f

    A continuous map from I to I that is monotone is directed

    source
    theorem DirectedUnitInterval.directed_path_bounded {t₀ t₁ : ↑unitInterval} {γ : Path t₀ t₁} (γ_dipath : IsDipath γ) (t : ↑unitInterval) :
    t₀ ≤ γ t ∧ γ t ≤ t₁

    A directed path on I is bounded by its source and target

    source
    theorem DirectedUnitInterval.directed_path_source_le_target {t₀ t₁ : ↑unitInterval} {γ : Path t₀ t₁} (γ_dipath : IsDipath γ) :
    t₀ ≤ t₁

    The source of a directed path on I is ≤ than its target