cons_le_of_notMem — Mathlib

English

If a ∉ s, then insert(a, s) ≤ t iff a ∈ t and s ≤ t.

Русский

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

LaTeX

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

Lean4

theorem cons_le_of_notMem (hs : a ∉ s) : a ::ₘ s ≤ t ↔ a ∈ t ∧ s ≤ t :=
  by
  apply Iff.intro (fun h ↦ ⟨subset_of_le h (mem_cons_self a s), le_trans (le_cons_self s a) h⟩)
  rintro ⟨h₁, h₂⟩; rcases exists_cons_of_mem h₁ with ⟨_, rfl⟩
  exact cons_le_cons _ ((le_cons_of_notMem hs).mp h₂)

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