ncard_subtype — Mathlib

English

The ncard of the subtype {x : Subtype P | x ∈ s} equals the ncard of the intersection s ∩ {x : P}

Русский

Кардинал подмножества {x : Subtype P | x ∈ s} равен кардиналу пересечения s с {x : P}

LaTeX

$$$ {x : Subtype P | (x:\alpha) \in s}.ncard = (s \cap setOf P).ncard $$$

Lean4

@[simp]
theorem ncard_subtype (P : α → Prop) (s : Set α) : {x : Subtype P | (x : α) ∈ s}.ncard = (s ∩ setOf P).ncard :=
  by
  convert (ncard_image_of_injective _ (@Subtype.coe_injective _ P)).symm
  ext x
  simp [← and_assoc, exists_eq_right]

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