ofSection_le_iff — Mathlib

English

For G, the principal a is contained in G if and only if x ∈ G.obj X.

Русский

Для G справедливо: \\mathrm{ofSection} x ≤ G тогда и только тогда, когда x ∈ G.obj X.

LaTeX

$$$ (\\mathrm{ofSection}\\ x) \\leq G \\iff x \\in G.\\mathrm{obj} X $$$

Lean4

@[simp]
theorem ofSection_le_iff (G : Subpresheaf F) : ofSection x ≤ G ↔ x ∈ G.obj X :=
  by
  constructor
  · intro hx
    exact hx _ (mem_ofSection_obj x)
  · rintro hx U _ ⟨f, rfl⟩
    exact G.map f hx

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