coe_smul — Mathlib

English

The underlying set of the smul of a flag by an order isomorphism equals the smul of the underlying set: ↑(e • s) = e • ↑s.

Русский

Подмножество, полученное при действии над флагом, совпадает с действием на основанном множестве: ↑(e • s) = e • ↑s.

LaTeX

$$\uparrow (e \cdot s) = e \cdot \uparrow s$$

Lean4

@[simp, norm_cast]
theorem coe_smul (e : α ≃o α) (s : Flag α) : (↑(e • s) : Set α) = e • s :=
  rfl

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