disjoint_iff — Mathlib

English

Equivalent form for disjointness using HasBasis, similar to the previous item.

Русский

Эквивалентная форма непересечения через HasBasis.

LaTeX

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

Lean4

theorem disjoint_iff (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
    Disjoint l l' ↔ ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i') :=
  not_iff_not.mp <| by
    simp only [_root_.disjoint_iff, ← Ne.eq_def, ← neBot_iff, inf_eq_inter, hl.inf_basis_neBot_iff hl', not_exists,
      not_and, bot_eq_empty, ← nonempty_iff_ne_empty]

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