disjoint_evalFrom_reverse_iff — Mathlib

English

For any x, S, S', the two disjointness relations are equivalent: Disjoint S (M.reverse.evalFrom S' x) holds iff Disjoint S' (M.evalFrom S x.reverse) holds.

Русский

Для любых x, S, S' равносильны два непересечения: Disjoint S (M.reverse.evalFrom S' x) и Disjoint S' (M.evalFrom S x.reverse).

LaTeX

$$Disjoint S (M.reverse.evalFrom S' x) \iff Disjoint S' (M.evalFrom S x.reverse)$$

Lean4

theorem disjoint_evalFrom_reverse_iff {x : List α} {S S' : Set σ} :
    Disjoint S (M.reverse.evalFrom S' x) ↔ Disjoint S' (M.evalFrom S x.reverse) :=
  ⟨disjoint_evalFrom_reverse, fun h ↦ List.reverse_reverse x ▸ disjoint_evalFrom_reverse h⟩

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