attachFin_ssubset_attachFin — Mathlib

English

If s is a strict subset of t, then s.attachFin with ht is a strict subset of t.attachFin ht.

Русский

Если s есть строгим подмножеством t, то соответствующее вложение s.attachFin строго вложено в t.attachFin ht.

LaTeX

$$s ⊂ t \\Rightarrow s.attachFin (fun m hm \\Rightarrow ht m (hst.subset hm)) ⊂ t.attachFin ht$$

Lean4

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

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