disjoint_stepSet_reverse — Mathlib

English

For any input a and sets S, S', the disjointness of S with the reverse-step-set S' a is equivalent to the disjointness of S' with the forward step-set S a.

Русский

Для любого символа a и множеств S, S' равенство непересечения S и forward(m.reverse).stepSet(S',a) эквивалентно непересечению S' и stepSet(S,a).

LaTeX

$$$Disjoint\ S\ (M.reverse.stepSet S'\, a) \iff Disjoint\ S'\ (M.stepSet\ S\ a)$$$

Lean4

theorem disjoint_stepSet_reverse {a : α} {S S' : Set σ} :
    Disjoint S (M.reverse.stepSet S' a) ↔ Disjoint S' (M.stepSet S a) :=
  by
  rw [← not_iff_not]
  simp only [Set.not_disjoint_iff, mem_stepSet, reverse_step, Set.mem_setOf_eq]
  tauto

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