le_def — Mathlib

English

For Subpresheaves S and T of F, S ≤ T iff for every U, S.obj U ≤ T.obj U (pointwise).

Русский

Для подпредPresheaf S и T над F верно S ≤ T тогда и только тогда, когда для каждого U выполняется S.obj U ≤ T.obj U (по точкам).

LaTeX

$$$\forall S,T:\mathrm{Subpresheaf}\ F,\ S \le T \iff \forall U:\mathrm{Opposite}(C),\ S.obj U \le T.obj U.$$$

Lean4

theorem le_def (S T : Subpresheaf F) : S ≤ T ↔ ∀ U, S.obj U ≤ T.obj U :=
  Iff.rfl

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