disjoint_iff_right — Mathlib

English

Let l have HasBasis p s. Then Disjoint l' l holds if and only if there exists i with p i and (s i)^c ∈ l'.

Русский

Пусть l имеет базис HasBasis p s. Тогда l' и l несовместны тогда и только тогда, когда существует i such that p i and (s i)^c ∈ l'.

LaTeX

$$$ l' \perp l \iff \exists i,\ p(i) \land (s(i))^c \in l' $$$

Lean4

theorem disjoint_iff_right (h : l.HasBasis p s) : Disjoint l' l ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l' :=
  disjoint_comm.trans h.disjoint_iff_left

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