dite_dite_comm — Mathlib

English

The nested dite and dite commute: (if p : P then A p else if q : Q then B q else C p q) = if q : Q then B q else if p : P then A p else C p q, under h : P → ¬Q.

Русский

Вложенное итерирование dite коммутирует: ... при условии h : P → ¬Q.

LaTeX

$$$\text{dite } P A B = \text{dite } Q B' C' \quad\text{(при допустимом } h)$$$

Lean4

theorem dite_dite_comm {B : Q → α} {C : ¬P → ¬Q → α} (h : P → ¬Q) :
    (if p : P then A p else if q : Q then B q else C p q) = if q : Q then B q else if p : P then A p else C p q := by
  grind

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