image_le_iff — Mathlib

English

For subpresheaf G of F, f: F → F', and G' ⊆ F', we have G.image f ≤ G' if and only if G ≤ G'.preimage f.

Русский

Для подпреша G ⊆ F, f: F → F' и G' ⊆ F', выполняется G.image f ≤ G' тогда и только тогда, когда G ≤ G'.preimage f.

LaTeX

$$$ G.\\mathrm{image} f \\leq G' \\;\\iff\\; G \\leq G'.\\mathrm{preimage} f $$$

Lean4

theorem image_le_iff (G : Subpresheaf F) (f : F ⟶ F') (G' : Subpresheaf F') : G.image f ≤ G' ↔ G ≤ G'.preimage f := by
  simp [Subpresheaf.le_def]

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