mem_attachFin — Mathlib

English

An element a of Fin n belongs to s.attachFin h if and only if the natural number a can be read as a member of s.

Русский

Элемент a из Fin n принадлежит s.attachFin h тогда и только тогда, когда соответствующее ему натуральное число принадлежит s.

LaTeX

$$a ∈ s.attachFin h \\iff (a : \\mathbb{N}) ∈ s$$

Lean4

@[simp]
theorem mem_attachFin {s : Finset ℕ} (h : ∀ m ∈ s, m < n) {a : Fin n} : a ∈ s.attachFin h ↔ (a : ℕ) ∈ s :=
  ⟨fun h ↦
    let ⟨_, hb₁, hb₂⟩ := Multiset.mem_pmap.1 h
    hb₂ ▸ hb₁,
    fun h ↦ Multiset.mem_pmap.2 ⟨a, h, Fin.eta _ _⟩⟩

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