mem_subtype — Mathlib

English

For p : α → Prop with decidable predicate, and s : Finset α, for any a : Subtype p, a ∈ s.subtype p iff (a : α) ∈ s.

Русский

Пусть p : α → Prop, с решаемым предикатом, и s : Finset α. Тогда для a : Subtype p выполняется: a ∈ s.subtype p ↔ (a : α) ∈ s.

LaTeX

$$a ∈ s.subtype p \\iff (a : α) ∈ s$$

Lean4

@[simp, grind =]
theorem mem_subtype {p : α → Prop} [DecidablePred p] {s : Finset α} : ∀ {a : Subtype p}, a ∈ s.subtype p ↔ (a : α) ∈ s
  | ⟨a, ha⟩ => by simp [Finset.subtype, ha]

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