down_inj

Mathlib.Logic.Function.ULift

URI: https://scilib.ai/kg/mathlib#PLift.down_inj

English

For any α and a,b ∈ PLift α, a.down = b.down iff a = b.

Русский

Для любых α и a,b ∈ PLift α верно: a.down = b.down тогда и только тогда, когда a = b.

LaTeX

$$$\\forall a,b:\\, \\mathrm{PLift}.\\down(a) = \\mathrm{PLift}.\\down(b) \\iff a = b$$$

Lean4

@[simp]
theorem down_inj {a b : PLift α} : a.down = b.down ↔ a = b :=
  ⟨fun h ↦ PLift.down_injective h, fun h ↦ by rw [h]⟩

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

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

Разделы

Аффилиация

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