supp_eq — Mathlib

English

The support of the constructor ⟨a, f⟩ is exactly the image of f on the universe, i.e., supp ⟨a, f⟩ = f'' univ.

Русский

Опора конструктора ⟨a, f⟩ равна образу f от всего множества: supp ⟨a, f⟩ = f'' univ.

LaTeX

$$$\mathrm{supp}\,⟨a, f⟩ = f''\,\mathrm{univ}.$$$

Lean4

theorem supp_eq {α : Type u} (a : P.A) (f : P.B a → α) : @supp.{u} P.Obj _ α (⟨a, f⟩ : P α) = f '' univ :=
  by
  ext x; simp only [supp, image_univ, mem_range, mem_setOf_eq]
  constructor <;> intro h
  · apply @h fun x => ∃ y : P.B a, f y = x
    rw [liftp_iff']
    intro
    exact ⟨_, rfl⟩
  · simp only [liftp_iff']
    cases h
    subst x
    tauto

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