iff_mpr_iff_true_intro

Mathlib.Logic.Basic

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

Lean4

theorem iff_mpr_iff_true_intro {P : Prop} (h : P) : Iff.mpr (iff_true_intro h) True.intro = h :=
  rfl

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

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

Разделы

Аффилиация

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