inf — Mathlib

English

The infimum of two HasBasis filters equals HasBasis on product indices with intersections of the corresponding sets.

Русский

Гранина между двумя фильтрами- базисами выражается через пересечение соответствующих множеств.

LaTeX

$$inf (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') : (l ⊓ l').HasBasis (fun i => And (p i.1) (p' i.2)) (fun i => s i.1 ∩ s' i.2)$$

Lean4

theorem inf {ι ι' : Type*} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : l.HasBasis p s)
    (hl' : l'.HasBasis p' s') : (l ⊓ l').HasBasis (fun i : ι × ι' => p i.1 ∧ p' i.2) fun i => s i.1 ∩ s' i.2 :=
  (hl.inf' hl').comp_equiv Equiv.pprodEquivProd.symm

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