le_cons_of_notMem — Mathlib

English

If a ∉ s, then s ≤ insert(a, t) is equivalent to s ≤ t.

Русский

Если a ∉ s, то s ≤ insert(a, t) эквивалентно s ≤ t.

LaTeX

$$$a \notin s \Rightarrow (s \le insert(a, t) \iff s \le t)$$$

Lean4

theorem le_cons_of_notMem (m : a ∉ s) : s ≤ a ::ₘ t ↔ s ≤ t :=
  by
  refine ⟨?_, fun h => le_trans h <| le_cons_self _ _⟩
  suffices ∀ {t'}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t' by exact fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))
  introv h
  revert m
  refine leInductionOn h ?_
  introv s m₁ m₂
  rcases append_of_mem m₂ with ⟨r₁, r₂, rfl⟩
  exact perm_middle.subperm_left.2 ((subperm_cons _).2 <| ((sublist_or_mem_of_sublist s).resolve_right m₁).subperm)

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