restrict_inj — Mathlib

English

Two compatible families on the sieve generated by R are equal if their restrictions to R are equal.

Русский

Две совместимые семьи на сгенерированном через R ситах равны, если их ограничения до R равны.

LaTeX

$$$x_1.Compatible \\to x_2.Compatible \\to (x_1.restrict( le\_generate(R) ) = x_2.restrict(le\_generate(R))) \Rightarrow x_1 = x_2$$$

Lean4

/-- Two compatible families on the sieve generated by a presieve `R` are equal if and only if they are
equal when restricted to `R`.
-/
theorem restrict_inj {x₁ x₂ : FamilyOfElements P (generate R).arrows} (t₁ : x₁.Compatible) (t₂ : x₂.Compatible) :
    x₁.restrict (le_generate R) = x₂.restrict (le_generate R) → x₁ = x₂ := fun h =>
  by
  rw [← extend_restrict t₁, ← extend_restrict t₂]
  congr

Похожие утверждения