card_subtype_eq_or_eq_of_ne — Mathlib

English

If a ≠ b in α, then the subtype { c ∈ α | c = a ∨ c = b } has cardinality 2.

Русский

Если a ≠ b в α, то подтип { c ∈ α | c = a ∨ c = b } имеет кардинал 2.

LaTeX

$$$$|\\{ c : α \\mid c = a \\lor c = b \\}| = 2.$$$$

Lean4

theorem card_subtype_eq_or_eq_of_ne {α : Type*} [Fintype α] [DecidableEq α] {a b : α} (h : a ≠ b) :
    Fintype.card { c : α // c = a ∨ c = b } = 2 :=
  Fintype.card_subtype_or_disjoint _ _ fun _ ha hb _ hc ↦ ha _ hc ▸ hb _ hc ▸ h <| rfl

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