disjoint — Mathlib

English

The boxes corresponding to ν and ν' are disjoint iff ν ≠ ν'.

Русский

Коробки соответствующие ν и ν' непересекаются тогда и только тогда, когда ν ≠ ν'.

LaTeX

$$$\nu \neq ν' \iff Disjoint(box(n,ν).toSet, box(n,ν').toSet)$$$

Lean4

theorem disjoint {ν ν' : ι → ℤ} : ν ≠ ν' ↔ Disjoint (box n ν).toSet (box n ν').toSet :=
  by
  rw [not_iff_comm, Set.not_disjoint_iff]
  refine ⟨fun ⟨x, hx, hx'⟩ ↦ ?_, fun h ↦ ⟨tag n ν, tag_mem n ν, h ▸ tag_mem n ν⟩⟩
  rw [← mem_box_iff_index.mp hx, ← mem_box_iff_index.mp hx']

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