of_map — Mathlib

English

If a predicate p on l would follow from p' on f(a), and (l.map f).Triplewise p', then l.Triplewise p.

Русский

Если предикат p на l следует из p' на f(a), и (l.map f).Triplewise p', тогда l.Triplewise p.

LaTeX

$$$$ (h : \\forall {a b c}, p'(f a)(f b)(f c) \\Rightarrow p a b c) \\rightarrow (hl : (l.map f).Triplewise p') \\rightarrow l.Triplewise p. $$$$

Lean4

theorem of_map (h : ∀ {a b c}, p' (f a) (f b) (f c) → p a b c) (hl : (l.map f).Triplewise p') : l.Triplewise p :=
  by
  rw [triplewise_map] at hl
  exact hl.imp h

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