OAI/GroupTheory/PolycyclicRecognition/Analysis/AffineFacetAgreement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Affine agreement on a facet determines the tangential linear part

  1. theorem OAI.PolycyclicRecognition.linear_eq_on_kernel_of_affine_facet_agreement line 15

    Source documentation

    Agreement on a relative neighborhood of a facet point implies agreement of linear parts on the entire parallel hyperplane.

    theorem linear_eq_on_kernel_of_affine_facet_agreement
    (A C : W →ₗ[ℝ] V) (b₁ b₂ : V) (ℓ : W →ₗ[ℝ] ℝ)
    (p : W) {ρ : ℝ} (hρ : 0 < ρ)
    (hagree : ∀ q, ℓ q = ℓ p → ‖q - p‖ < ρ → A q + b₁ = C q + b₂) :
    ∀ w, ℓ w = 0 → A w = C w := by
…