coe_mono — Mathlib

English

SetLike.coe is monotone with respect to the subset order: if p ≤ q then the underlying sets satisfy coe(p) ⊆ coe(q).

Русский

SetLike.coe монотонна относительно порядка подмножеств: если p ≤ q, то coe(p) ⊆ coe(q).

LaTeX

$$$ p \le q \Rightarrow (\mathrm{SetLike}.coe\ p) \subseteq (\mathrm{SetLike}.coe\ q) $$$

Lean4

@[mono]
theorem coe_mono : Monotone (SetLike.coe : A → Set B) := fun _ _ => coe_subset_coe.mpr

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