coe_wcovBy_coe — Mathlib

English

The covering relation for Finsets, when viewed as sets, agrees with the covering relation in the set-theoretic order.

Русский

Покрывающие отношения Finset, рассматриваемые как множества, согласуются с покрывающим отношением в порядке множеств.

LaTeX

$$$ (s : Set\alpha) \; \triangleleft\; t \iff s \triangleleft t $$$

Lean4

@[simp]
theorem coe_wcovBy_coe : (s : Set α) ⩿ t ↔ s ⩿ t :=
  ordConnected_range_coe.apply_wcovBy_apply_iff ⟨⟨_, coe_injective⟩, coe_subset⟩

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