mk_div_mk — Mathlib

English

If hx ≥ 0 and hy ≥ 0, then (⟨x,hx⟩) / ⟨y,hy⟩ = ⟨x/y, div_nonneg hx hy⟩.

Русский

Если hx ≥ 0 и hy ≥ 0, то (⟨x,hx⟩) / ⟨y,hy⟩ = ⟨x/y, div_nonneg hx hy⟩.

LaTeX

$$$\\text{mk\\_div\\_mk} \\; (hx:\\ge 0 x) (hy:\\ge 0 y): (⟨x, hx⟩ : { x : α // 0 ≤ x }) / ⟨y, hy⟩ = ⟨x / y, div\\_nonneg hx hy⟩$$$

Lean4

@[simp]
theorem mk_div_mk (hx : 0 ≤ x) (hy : 0 ≤ y) : (⟨x, hx⟩ : { x : α // 0 ≤ x }) / ⟨y, hy⟩ = ⟨x / y, div_nonneg hx hy⟩ :=
  rfl

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