liftp_iff' — Mathlib

English

Specialized equivalence: for a fixed a and f, Liftp p ⟨a, f⟩ is equivalent to ∀ i, p (f i).

Русский

Специализированное описание: для данного a и f, Liftp p ⟨a, f⟩ эквивалентно ∀ i, p (f i).

LaTeX

$$$@Liftp.{u} P.Obj _ α p \langle a, f\rangle \iff \forall i, p (f i).$$$

Lean4

theorem liftp_iff' {α : Type u} (p : α → Prop) (a : P.A) (f : P.B a → α) :
    @Liftp.{u} P.Obj _ α p ⟨a, f⟩ ↔ ∀ i, p (f i) :=
  by
  simp only [liftp_iff]; constructor <;> intro h
  · rcases h with ⟨a', f', heq, h'⟩
    cases heq
    assumption
  repeat'
    first
    | constructor
    | assumption

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