isSeparatedFor_iff_generate — Mathlib

English

IsSeparatedFor P R holds iff IsSeparatedFor P (generate R).arrows, i.e., separating property is preserved when passing to the generated sieve.

Русский

Свойство раздельности P для R эквивалентно раздельности P для порождаемого сепаратора generate R, то есть свойство сохраняется при переходе к генерируемому ситу.

LaTeX

$$IsSeparatedFor P R ↔ IsSeparatedFor P (generate R).arrows$$

Lean4

theorem isSeparatedFor_iff_generate : IsSeparatedFor P R ↔ IsSeparatedFor P (generate R : Presieve X) :=
  by
  constructor
  · intro h x t₁ t₂ ht₁ ht₂
    apply h (x.restrict (le_generate R)) t₁ t₂ _ _
    · exact isAmalgamation_restrict _ x t₁ ht₁
    · exact isAmalgamation_restrict _ x t₂ ht₂
  · intro h x t₁ t₂ ht₁ ht₂
    apply h x.sieveExtend
    · exact isAmalgamation_sieveExtend x t₁ ht₁
    · exact isAmalgamation_sieveExtend x t₂ ht₂

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