CertificateNeighborhoods.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.finite_eventual_neighborhoods line 16

Source documentation

Finitely many eventual properties hold simultaneously on balls with one common positive radius around their respective centers.

theorem finite_eventual_neighborhoods {ι : Type uIndex} {X : Type uX} [PseudoMetricSpace X]
    (s : Finset ι) (p : ι → X) (P : ι → X → Prop)
    (hP : ∀ i ∈ s, ∀ᶠ x in nhds (p i), P i x) :
    ∃ r : ℝ, 0 < r ∧ ∀ i ∈ s, ∀ x, dist x (p i) < r → P i x := by
…

theorem OAI.Problem356.finite_eventual_triple_neighborhoods line 39

Source documentation

Triple-coordinate ball version of finite eventual shrinking.

theorem finite_eventual_triple_neighborhoods {ι : Type uIndex}
    (s : Finset ι) (p : ι → Triple) (P : ι → Triple → Prop)
    (hP : ∀ i ∈ s, ∀ᶠ t in nhds (p i), P i t) :
    ∃ r : ℝ, 0 < r ∧ ∀ i ∈ s, ∀ x y z : E3,
      x ∈ ball (p i).1 r → y ∈ ball (p i).2.1 r →
      z ∈ ball (p i).2.2 r → P i (x, (y, z)) := by
…

Mentions: OAI.Problem356.Triple, OAI.Problem356.E3

theorem OAI.Problem356.finite_strict_neighborhoods line 54

Source documentation

Finitely many strict inequalities at their respective centers persist on one common positive-radius neighborhood. This is the finite shrinking step for the bad, distinct-center component types in the certificate.

theorem finite_strict_neighborhoods {ι : Type uIndex} {X : Type uX} {Y : Type uY} [PseudoMetricSpace X]
    [TopologicalSpace Y] [LinearOrder Y] [OrderClosedTopology Y]
    (s : Finset ι) (p : ι → X) (f g : ι → X → Y)
    (hf : ∀ i ∈ s, ContinuousAt (f i) (p i))
    (hg : ∀ i ∈ s, ContinuousAt (g i) (p i))
    (hgap : ∀ i ∈ s, f i (p i) < g i (p i)) :
    ∃ r : ℝ, 0 < r ∧ ∀ i ∈ s, ∀ x, dist x (p i) < r → f i x < g i x := by
…

theorem OAI.Problem356.finite_strict_triple_neighborhoods line 66

Source documentation

Product-space version of finite shrinking, expressed by separate ball conditions on all three coordinates.

theorem finite_strict_triple_neighborhoods {ι : Type uIndex} {Y : Type uY}
    [TopologicalSpace Y] [LinearOrder Y] [OrderClosedTopology Y]
    (s : Finset ι) (p : ι → Triple) (f g : ι → Triple → Y)
    (hf : ∀ i ∈ s, ContinuousAt (f i) (p i))
    (hg : ∀ i ∈ s, ContinuousAt (g i) (p i))
    (hgap : ∀ i ∈ s, f i (p i) < g i (p i)) :
    ∃ r : ℝ, 0 < r ∧ ∀ i ∈ s, ∀ x y z : E3,
      x ∈ ball (p i).1 r → y ∈ ball (p i).2.1 r →
      z ∈ ball (p i).2.2 r → f i (x, (y, z)) < g i (x, (y, z)) := by
…

Mentions: OAI.Problem356.Triple, OAI.Problem356.E3