subperm_singleton_iff — Mathlib

English

A list l is a subpermutation of the singleton [a] if and only if l is empty or l is equal to [a].

Русский

Список l является подпермутацией одиночного списка [a], если и только если l пуст или l = [a].

LaTeX

$$$l <+~ [a] \iff (l = [] \lor l = [a])$$$

Lean4

@[simp]
theorem subperm_singleton_iff : l <+~ [a] ↔ l = [] ∨ l = [a] :=
  by
  constructor
  · rw [subperm_iff]
    rintro ⟨s, hla, h⟩
    rwa [perm_singleton.mp hla, sublist_singleton] at h
  · rintro (rfl | rfl)
    exacts [nil_subperm, Subperm.refl _]

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