coe_insert — Mathlib

English

The embedding respects insertion: the embedded insert equals the class insertion.

Русский

Встроенная операция вставки сохраняется: встроение вставки равно вставке в контексте класса.

LaTeX

$$$\\uparrow(\\operatorname{insert}(x,y)) = @\\mathrm{insert} \\ZFSet\\Class\\_ \\ x\\ y$$$

Lean4

@[simp, norm_cast]
theorem coe_insert (x y : ZFSet.{u}) : ↑(insert x y) = @insert ZFSet.{u} Class.{u} _ x y :=
  ext fun _ => ZFSet.mem_insert_iff

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