RectangleCrossing.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Two transverse continuous crossings of a rectangle intersect, by Brouwer's fixed-point theorem and the two-dimensional Poincaré–Miranda argument. No simplicity or regularity of the crossing is needed.

def OAI.SLEExactGauge.RectangleCrossing.clampUnit line 16
theorem OAI.SLEExactGauge.RectangleCrossing.clampUnit_mem line 18
theorem OAI.SLEExactGauge.RectangleCrossing.clampUnit_continuous line 21
theorem OAI.SLEExactGauge.RectangleCrossing.clampUnit_fixed_forces_zero line 25
def OAI.SLEExactGauge.RectangleCrossing.unitSquare line 47

theorem OAI.SLEExactGauge.RectangleCrossing.poincare_miranda_square line 51

Source documentation

The rectangle intermediate-value theorem with signs on its four faces. The map can have arbitrary behavior in the interior.

theorem poincare_miranda_square
    (F : ℝ × ℝ → ℝ × ℝ) (hF : ContinuousOn F unitSquare)
    (hleft : ∀ y ∈ Icc (0 : ℝ) 1, (F (0, y)).1 ≤ 0)
    (hright : ∀ y ∈ Icc (0 : ℝ) 1, 0 ≤ (F (1, y)).1)
    (hbottom : ∀ x ∈ Icc (0 : ℝ) 1, (F (x, 0)).2 ≤ 0)
    (htop : ∀ x ∈ Icc (0 : ℝ) 1, 0 ≤ (F (x, 1)).2) :
    ∃ z ∈ unitSquare, F z = (0, 0) := by
…

Mentions: OAI.SLEExactGauge.RectangleCrossing.unitSquare

theorem OAI.SLEExactGauge.RectangleCrossing.paths_intersect_rectangle line 81

Source documentation

A longitudinal crossing and a transverse crossing of any nondegenerate axis-aligned rectangle meet, even when either path has self-intersections.

theorem paths_intersect_rectangle
    (p q : ℝ → ℂ) (a b c d : ℝ) (_hab : a < b) (_hcd : c < d)
    (hp : ContinuousOn p (Icc 0 1)) (hq : ContinuousOn q (Icc 0 1))
    (hpr : ∀ t ∈ Icc (0 : ℝ) 1, (p t).re ∈ Icc a b ∧ (p t).im ∈ Icc c d)
    (hqr : ∀ t ∈ Icc (0 : ℝ) 1, (q t).re ∈ Icc a b ∧ (q t).im ∈ Icc c d)
    (hp0 : (p 0).re = a) (hp1 : (p 1).re = b)
    (hq0 : (q 0).im = c) (hq1 : (q 1).im = d) :
    ∃ s ∈ Icc (0 : ℝ) 1, ∃ t ∈ Icc (0 : ℝ) 1, p s = q t := by
…