le_def — Mathlib

English

The pointwise order on Pretopologies coincides with the order coming from their assigned coverings: K1 ≤ K2 if and only if for every X, K1 X ⊆ K2 X.

Русский

Пусть K1, K2 — препотопологии на C. Тогда порядок между ними определяется по покрытиям: K1 ≤ K2 тогда и только тогда, когда для каждого объекта X выполняется K1 X ⊆ K2 X.

LaTeX

$$$K_1 \\le K_2 \\iff \\forall X,\\ (K_1 X) \\subseteq (K_2 X).$$$

Lean4

theorem le_def {K₁ K₂ : Pretopology C} : K₁ ≤ K₂ ↔ (K₁ : ∀ X : C, Set (Presieve X)) ≤ K₂ :=
  Iff.rfl

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