card_lt_univ_of_notMem — Mathlib

English

Let α be finite and s a finite subset of α, and x ∈ α with x ∉ s. Then |s| < |Fintype α|.

Русский

Пусть α конечно, s ⊆ α и x ∈ α такой, что x ∉ s. Тогда |s| < |α|.

LaTeX

$$$\forall \alpha [Fintype \alpha], \forall s : Finset \alpha, \forall x : \alpha, x \notin s \Rightarrow |s| < |\alpha|$$$

Lean4

theorem card_lt_univ_of_notMem [Fintype α] {s : Finset α} {x : α} (hx : x ∉ s) : #s < Fintype.card α :=
  card_lt_card ⟨subset_univ s, not_forall.2 ⟨x, fun hx' => hx (hx' <| mem_univ x)⟩⟩

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