comap — Mathlib

English

If s is Antitone and ι is directed with a nonempty index set, then the infimum of principal(s i) has an antitone basis given by s.

Русский

Если s антитоничен и индексный набор непуст, инфимума по principal(s i) имеет базис, заданный s.

LaTeX

$$$ (\iInf i, \mathcal P(s(i))).HasAntitoneBasis s $$$

Lean4

protected theorem comap {l : Filter α} {s : ι'' → Set α} (hf : HasAntitoneBasis l s) (m : β → α) :
    HasAntitoneBasis (comap m l) (m ⁻¹' s ·) :=
  ⟨hf.1.comap _, fun _ _ h ↦ preimage_mono (hf.2 h)⟩

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