attachFin_subset_attachFin — Mathlib

English

If s ⊆ t and every element of t is below n, then s.attachFin maps into t.attachFin via ht.

Русский

Если s ⊆ t и каждый элемент t мале н, то s.attachFin отображается в t.attachFin через ht.

LaTeX

$$s ⊆ t \\Rightarrow s.attachFin (fun m hm ↦ ht m (hst hm)) ⊆ t.attachFin ht$$

Lean4

@[mono, gcongr]
theorem attachFin_subset_attachFin {s t : Finset ℕ} (hst : s ⊆ t) (ht : ∀ m ∈ t, m < n) :
    s.attachFin (fun m hm ↦ ht m (hst hm)) ⊆ t.attachFin ht := by simpa

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