fintypeInterOfLeft — Mathlib

English

A Finite type instance exists for s ∩ t when s is finite, using those elements of s that lie in t.

Русский

Существует экземпляр конечного типа для s ∩ t, когда s конечно, через элементы s, принадлежащие t.

LaTeX

$$$ Fintype( s \cap t ) $$$

Lean4

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

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