optionSubtypeNe_symm_of_ne — Mathlib

English

If b ≠ a, then (optionSubtypeNe a).symm b = some ⟨b, h⟩ for the corresponding witness h.

Русский

Если b ≠ a, то (optionSubtypeNe a).symm b = some ⟨b, h⟩ для соответствующего свидетельства h.

LaTeX

$$$\text{If } b ≠ a,\; (\mathrm{optionSubtypeNe}\ a).\mathrm{symm}\ b = \mathrm{some}\langle b, h\rangle.$$$

Lean4

theorem optionSubtypeNe_symm_of_ne (hba : b ≠ a) : (optionSubtypeNe a).symm b = some ⟨b, hba⟩ := by simp [hba]

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