fintypeInterOfRight — Mathlib

English

Let s and t be subsets of a type α. If t is finite, then the intersection s ∩ t is finite.

Русский

Пусть s и t — множества над множеством α. Если t конечно, то пересечение s ∩ t конечно.

LaTeX

$$$\\forall \\alpha\\, (s,t : \\text{Set }\\alpha),\\; \\operatorname{Finite}(t) \\Rightarrow \\operatorname{Finite}(s \\cap t).$$$

Lean4

/-- A `Fintype` instance for set intersection where the right set has a `Fintype` instance. -/
instance fintypeInterOfRight (s t : Set α) [Fintype t] [DecidablePred (· ∈ s)] : Fintype (s ∩ t : Set α) :=
  Fintype.ofFinset ({a ∈ t.toFinset | a ∈ s}) <| by simp [and_comm]

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