perm_option_toList — Mathlib

English

Two options o1 and o2 are permutation-equivalent exactly when they are equal as options.

Русский

Два значения типа option эквивалентны перестановке тогда и только тогда, когда они равны как опции.

LaTeX

$$$o_1^{\\to\\mathrm{List}} ~ o_2^{\\to\\mathrm{List}} \\iff o_1 = o_2$$$

Lean4

theorem perm_option_toList {o₁ o₂ : Option α} : o₁.toList ~ o₂.toList ↔ o₁ = o₂ :=
  by
  refine ⟨fun p => ?_, fun e => e ▸ Perm.refl _⟩
  rcases o₁ with - | a <;> rcases o₂ with - | b; · rfl
  · cases p.length_eq
  · cases p.length_eq
  · exact Option.mem_toList.1 (p.symm.subset <| by simp)

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