exists_mem_filter_basis — Mathlib

English

If l and l' are disjoint, then there exist basis indices i, i' with p i, p' i' such that s i and s' i' are disjoint.

Русский

Если фильтры l и l' не пересекаются, то найдутся базисные индексы i и i' такие, что s i и s' i' дисjoint.

LaTeX

$$$\\exists i, p i \\land \\exists i', p' i' \\land \\text{Disjoint}(s i, s' i')$$$

Lean4

theorem _root_.Disjoint.exists_mem_filter_basis (h : Disjoint l l') (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
    ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i') :=
  (hl.disjoint_iff hl').1 h

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