compatible_iff_sieveCompatible — Mathlib

English

There is a natural equivalence between compatible families on R and compatible families on generate R via restriction and sieve-extension.

Русский

Существуют естественные эквивалентности между совместимыми семействами на R и на generate R через ограничение и расширение сита.

LaTeX

$$$\\{ x : FamilyOfElements P R \\;\\text{with } x.Compatible \\} \\simeq \\{ x : FamilyOfElements P (\\text{generate } R) \\;\\text{with } x.Compatible \\}$ via (restrict, sieveExtend)$$

Lean4

theorem compatible_iff_sieveCompatible (x : FamilyOfElements P (S : Presieve X)) : x.Compatible ↔ x.SieveCompatible :=
  by
  constructor
  · intro h Y Z f g hf
    simpa using h (𝟙 _) g (S.downward_closed hf g) hf (id_comp _)
  · intro h Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ k
    simp_rw [← h f₁ g₁ h₁, ← h f₂ g₂ h₂]
    congr

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