prod — Mathlib

English

If ha and gb are HasAntitoneBasis on sa and tb, then their product has HasAntitoneBasis sa(i) × tb(i).

Русский

Если ha и gb являются антитональными базисами на sa и tb, то их произведение обладает антитональным базисом sa(i) × tb(i).

LaTeX

$$HasAntitoneBasis.prod ha gb.$$

Lean4

theorem prod {ι : Type*} [LinearOrder ι] {f : Filter α} {g : Filter β} {s : ι → Set α} {t : ι → Set β}
    (hf : HasAntitoneBasis f s) (hg : HasAntitoneBasis g t) : HasAntitoneBasis (f ×ˢ g) fun n => s n ×ˢ t n :=
  ⟨hf.1.prod_same_index_anti hg.1 (hf.2.antitoneOn _) (hg.2.antitoneOn _), hf.2.set_prod hg.2⟩

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