rel_filterMap — Mathlib

English

Let f and g be functions into an output type, and let R be a relation on the inputs. Then filterMap respects a relation lifting: filtering with f on the left and g on the right preserves a Forall₂ relation between input lists and the corresponding output lists, provided the relation between outputs is given by a lifted P.

Русский

Пусть f,g — функции, затем filterMap сохраняет отображение относительного поднятия: отбор с помощью f слева и g справа сохраняет связь Forall₂ между входными списками и соответствующими выходами, при условии, что отношение выходов задано подъемом P.

LaTeX

$$$$\\text{rel\\_filterMap: } ((R \\Rightarrow \\mathrm{Option.Rel\\ P}) \\Rightarrow \\mathrm{Forall_2 R} \\Rightarrow \\mathrm{Forall_2 P})\\ \\mathrm{filterMap} \\ \\mathrm{filterMap} $$$$

Lean4

theorem rel_filterMap : ((R ⇒ Option.Rel P) ⇒ Forall₂ R ⇒ Forall₂ P) filterMap filterMap
  | _, _, _, _, _, Forall₂.nil => Forall₂.nil
  | f, g, hfg, a :: as, b :: bs, Forall₂.cons h₁ h₂ =>
    by
    rw [filterMap_cons, filterMap_cons]
    exact
      match f a, g b, hfg h₁ with
      | _, _, Option.Rel.none => rel_filterMap (@hfg) h₂
      | _, _, Option.Rel.some h => Forall₂.cons h (rel_filterMap (@hfg) h₂)

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