dite_ne_left_iff — Mathlib

English

Let α be a type, P a Prop, and a : α; assume a is never equal to B h for all h when considering the left branch of dite. Then dite P (const a) B ≠ a ⇔ ¬P.

Русский

Пусть α — множество, P — Prop, и пусть a : α. Предположим, что в левой ветви dite всегда получается значение a, отличное от B h. Тогда dite P (константа a) B ≠ a эквивалентно ¬P.

LaTeX

$$$(dite P (fun _ => a) B) \neq a \iff \lnot P$$$

Lean4

protected theorem dite_ne_left_iff (h : ∀ h, a ≠ B h) : dite P (fun _ ↦ a) B ≠ a ↔ ¬P :=
  dite_ne_left_iff.trans <| exists_iff_of_forall h

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