dite_ne_right_iff — Mathlib

English

Let α be a type, P a Prop, and b : α; assume A h ≠ b for all h on the right branch of dite. Then (dite P A (λ _ => b)) ≠ b ⇔ P.

Русский

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

LaTeX

$$$(dite P A (fun _ => b)) \neq b \iff P$$$

Lean4

protected theorem dite_ne_right_iff (h : ∀ h, A h ≠ b) : (dite P A fun _ ↦ b) ≠ b ↔ P :=
  dite_ne_right_iff.trans <| exists_iff_of_forall h

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