principal_inf — Mathlib

English

For l with basis p, s and l' with p', s', NeBot(l ⊓ l') iff for all i, p i and all i', p' i' imply (s i ∩ s' i').Nonempty.

Русский

Для фильтра с базисом l и l' с базисом их пересечения NeBot(l ⊓ l') эквивалентно: для всех i, p i и для всех i', p' i' следует, что (s_i ∩ s'_i'). непусто.

LaTeX

$$$\\text{Inf Basis NeBot Iff}\\left(l, l'\\right)\\iff \\forall i, p i \\to \\forall i', p' i' \\to (s i \\cap s' i').Nonempty$$$

Lean4

theorem principal_inf (hl : l.HasBasis p s) (s' : Set α) : (𝓟 s' ⊓ l).HasBasis p fun i => s' ∩ s i := by
  simpa only [inf_comm, inter_comm] using hl.inf_principal s'

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