dite_ne_right_iff

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#dite_ne_right_iff

English

The statement (dite P A (λ _ , b)) ≠ b is equivalent to there exists h with A h ≠ b.

Русский

Неравенство (dite P A (λ _ , b)) ≠ b эквивалентно существованию h, такого что A(h) ≠ b.

LaTeX

$$$(\mathrm{dite}\, P\, A\, (\lambda\_\to b)) \neq b \iff \exists h, A(h) \neq b.$$$

Lean4

theorem dite_ne_right_iff : (dite P A fun _ ↦ b) ≠ b ↔ ∃ h, A h ≠ b := by simp only [Ne, dite_eq_right_iff, not_forall]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru