attachFin_subset_attachFin_iff — Mathlib

English

Given bounds hs and ht ensuring all elements are below n, s.attachFin hs ⊆ t.attachFin ht iff s ⊆ t.

Русский

При задании границ hs, ht так, чтобы все элементы были меньше n, s.attachFin hs ⊆ t.attachFin ht тогда и только тогда, когда s ⊆ t.

LaTeX

$$s.attachFin hs ⊆ t.attachFin ht \\Leftrightarrow s ⊆ t$$

Lean4

@[simp]
theorem attachFin_subset_attachFin_iff {s t : Finset ℕ} (hs : ∀ m ∈ s, m < n) (ht : ∀ m ∈ t, m < n) :
    s.attachFin hs ⊆ t.attachFin ht ↔ s ⊆ t := by simp [← map_subset_map (f := Fin.valEmbedding)]

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