liftP_iff' — Mathlib

English

A specialized form of liftP_iff: LiftP p x is equivalent to the existence of a pair ⟨a, f⟩ such that x = ⟨a, f⟩ and p (f i j) holds for all i, j.

Русский

Упрощённая форма liftP: LiftP p x эквивалентно существованию пары ⟨a, f⟩ такому, что x = ⟨a, f⟩ и p (f i j) для всех i, j выполняется.

LaTeX

$$$\\text{LiftP } p\\, x \\;\\Longleftrightarrow\\; \\exists a\\, f,\\ x = \\langle a, f \\rangle \\land \\forall i j, p (f i j)$$$

Lean4

theorem liftP_iff' {α : TypeVec n} (p : ∀ ⦃i⦄, α i → Prop) (a : P.A) (f : P.B a ⟹ α) :
    @LiftP.{u} _ P.Obj _ α p ⟨a, f⟩ ↔ ∀ i x, p (f i x) :=
  by
  simp only [liftP_iff]; constructor
  · rintro ⟨_, _, ⟨⟩, _⟩
    assumption
  · intro
    repeat'
      first
      | constructor
      | assumption

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