of_eq — Mathlib

English

An explicit restatement: For any α,β types with Primcodable instances, if hr is PrimrecRel r and H holds pointwise, then PrimrecRel s.

Русский

Повторное формулирование: для любых типов α, β с примитивно кодируемыми структурами, если hr = PrimrecRel r и выполнено поэлементарное равенство, то PrimrecRel s.

LaTeX

$$$\operatorname{PrimrecRel} r \to (\forall a,b, r(a,b) \leftrightarrow s(a,b)) \to \operatorname{PrimrecRel} s$$$

Lean4

theorem of_eq {α β} [Primcodable α] [Primcodable β] {r s : α → β → Prop} (hr : PrimrecRel r)
    (H : ∀ a b, r a b ↔ s a b) : PrimrecRel s :=
  funext₂ (fun a b => propext (H a b)) ▸ hr

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