exists_notMem_of_length_lt — Mathlib

English

For any list l, if its length is strictly less than the cardinality of α, there exists an element z not in l.

Русский

Для любого списка l, если длина l строго меньше кардинала α, существует элемент z, который не входит в l.

LaTeX

$$$\\exists z:\\alpha, z \\notin l$ given $↑l.length < #\\alpha$$$

Lean4

theorem exists_notMem_of_length_lt {α : Type*} (l : List α) (h : ↑l.length < #α) : ∃ z : α, z ∉ l := by
  classical
  contrapose! h
  calc
    #α = #(Set.univ : Set α) := mk_univ.symm
    _ ≤ #l.toFinset := (mk_le_mk_of_subset fun x _ => List.mem_toFinset.mpr (h x))
    _ = l.toFinset.card := Cardinal.mk_coe_finset
    _ ≤ l.length := Nat.cast_le.mpr (List.toFinset_card_le l)

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