guard_eq_some'

Mathlib.Data.Option.Basic

URI: https://scilib.ai/kg/mathlib#Option.guard_eq_some'

English

The guard of a proposition equals some unit if and only if the proposition is true (with decidability).

Русский

Guard(p) = some(u) эквивалентно p, при наличии decidable p.

LaTeX

$$$$ \forall {p} [\mathrm{Decidable}(p)], \mathrm{guard}(p) = \mathrm{some}(u) \iff p. $$$$

Lean4

@[simp]
theorem guard_eq_some' {p : Prop} [Decidable p] (u) : _root_.guard p = some u ↔ p := by
  grind [cases Option, _root_.guard]

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

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

Разделы

Аффилиация

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