coe_finsetInf — Mathlib

English

For a finite index set, the underlying set of the finite infimum equals the intersection over indices.

Русский

Для конечного множества индексов подмодуля: основание ∑ inf совпадает с пересечением по индексам.

LaTeX

$$$\uparrow(\text{Finset}.inf\, p) = \bigcap_{i \in s} \uparrow(p(i))$$$

Lean4

@[simp]
theorem coe_finsetInf {ι} (s : Finset ι) (p : ι → Submodule R M) : (↑(s.inf p) : Set M) = ⋂ i ∈ s, ↑(p i) :=
  by
  letI := Classical.decEq ι
  refine s.induction_on ?_ fun i s _ ih ↦ ?_
  · simp
  · rw [Finset.inf_insert, coe_inf, ih]
    simp

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