preimage_eq_top_iff — Mathlib

English

For G ⊆ F and p: F' → F, the preimage G under p equals top if and only if the range of p is contained in G.

Русский

Для G ⊆ F и p: F' → F, предобраз G по p равен верху тогда и только тогда, когда образ (range) p содержится в G.

LaTeX

$$$ G.\\mathrm{preimage} p = \\top \\quad\\text{iff}\\quad \\mathrm{range}\,p \\le G $$$

Lean4

theorem preimage_eq_top_iff (G : Subpresheaf F) (p : F' ⟶ F) : G.preimage p = ⊤ ↔ range p ≤ G :=
  by
  rw [← image_top, image_le_iff]
  simp

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