coe_inter — Mathlib

English

The coercion of the intersection equals the intersection of the coerced sets: ↑(s1 ∩ s2) = (s1 ∩ s2) as Set.

Русский

Приведение пересечения к множеству равно пересечению приводимых множеств.

LaTeX

$$$\\uparrow (s_{1} \\cap s_{2}) = (s_{1} \\cap s_{2}) \\,:\\, \\text{Set}$$$

Lean4

@[simp, norm_cast]
theorem coe_inter (s₁ s₂ : Finset α) : ↑(s₁ ∩ s₂) = (s₁ ∩ s₂ : Set α) :=
  Set.ext fun _ => mem_inter

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