uniformity_lift_le_comp — Mathlib

English

For monotone f, ((𝓤 α).lift (λ s, f (s ○ s))) ≤ (𝓤 α).lift f.

Русский

Для монотонной f выполняется ((𝓤 α).lift (λ s, f (s ○ s))) ≤ (𝓤 α).lift f.

LaTeX

$$$$\\text{If } f\\text{ is monotone } ((𝓤 α).lift\\; (\\lambda s, f (s \\circ s))) \\le (𝓤 α).lift f.$$$$

Lean4

theorem uniformity_lift_le_comp {f : Set (α × α) → Filter β} (h : Monotone f) :
    ((𝓤 α).lift fun s => f (s ○ s)) ≤ (𝓤 α).lift f :=
  calc
    ((𝓤 α).lift fun s => f (s ○ s)) = ((𝓤 α).lift' fun s : Set (α × α) => s ○ s).lift f :=
      by
      rw [lift_lift'_assoc]
      · exact monotone_id.compRel monotone_id
      · exact h
    _ ≤ (𝓤 α).lift f := lift_mono comp_le_uniformity le_rfl

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