blur' — Mathlib

English

A construction blur' replaces the underlying set of a Semiquot by a specified superset.

Русский

Конструкция blur' заменяет множество основания семикуота на заданное надмножество.

LaTeX

$$$(blur'(q,h)).s = s$$$

Lean4

/-- Replace `s` in a `Semiquot` with a superset. -/
def blur' (q : Semiquot α) {s : Set α} (h : q.s ⊆ s) : Semiquot α :=
  ⟨s, Trunc.lift (fun a : q.s => Trunc.mk ⟨a.1, h a.2⟩) (fun _ _ => Trunc.eq _ _) q.2⟩

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