instHImp — Mathlib

English

There is a Heyting implication on a product type defined coordinatewise: (a1,a2) ⇨ (b1,b2) = (a1 ⇨ b1, a2 ⇨ b2).

Русский

Для произведения типов существует импликация Хейтинга, заданная покоординатно: (a1,a2) ⇨ (b1,b2) = (a1 ⇨ b1, a2 ⇨ b2).

LaTeX

$$(a_1, a_2) \\Rightarrow (b_1, b_2) = (a_1 \\Rightarrow b_1, a_2 \\Rightarrow b_2)$$

Lean4

instance instHImp [HImp α] [HImp β] : HImp (α × β) :=
  ⟨fun a b => (a.1 ⇨ b.1, a.2 ⇨ b.2)⟩

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