Theorems · Theorem · algebraic geometry

AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux

∀ {X : TopCat} (F : TopCat.Presheaf CommRingCat X) {U₁ U₂ U₃ U₄ U₅ U₆ U₇ : TopologicalSpace.Opens ↑X} {n₁ n₂ : ℕ}
  {y₁ : ↑(F.obj (Opposite.op U₁))} {y₂ : ↑(F.obj (Opposite.op U₂))} {f : ↑(F.obj (Opposite.op (U₁ ⊔ U₂)))}
  {x : ↑(F.obj (Opposite.op U₃))} (h₄₁ : U₄ ≤ U₁) (h₄₂ : U₄ ≤ U₂) (h₅₁ : U₅ ≤ U₁) (h₅₃ : U₅ ≤ U₃) (h₆₂ : U₆ ≤ U₂)
  (h₆₃ : U₆ ≤ U₃) (h₇₄ : U₇ ≤ U₄),
  U₇ ≤ U₅ →
    U₇ ≤ U₆ →
      TopCat.Presheaf.restrictOpen y₁ U₅ h₅₁ =
          TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯) U₅ h₅₁ ^ n₁ *
            TopCat.Presheaf.restrictOpen x U₅ h₅₃ →
        TopCat.Presheaf.restrictOpen y₂ U₆ h₆₂ =
            TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯) U₆ h₆₂ ^ n₂ *
              TopCat.Presheaf.restrictOpen x U₆ h₆₃ →
          TopCat.Presheaf.restrictOpen
              (TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯ ^ n₂ * y₁) U₄ h₄₁) U₇ h₇₄ =
            TopCat.Presheaf.restrictOpen
              (TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯ ^ n₁ * y₂) U₄ h₄₂) U₇ h₇₄

Defined in

Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Cited by

1 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound