image_op_one — Mathlib

English

Let α be a type with a distinguished order and MulOpposite structure. The image of the singleton {1} under the opposite map equals {1}.

Русский

Пусть имеется перевод между типом и его противоположностью; образ множества {1} под операцией противоположности равен {1}.

LaTeX

$$$ \mathrm{image}(\mathrm{op}, \{1\}) = \{1\} $$$

Lean4

@[to_additive (attr := simp)]
theorem image_op_one [DecidableEq α] : (1 : Finset α).image op = 1 :=
  rfl

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