instIsStrictlySupportedStupidTrunc_1

English

If K is strictly supported relative to some embedding e', then K.stupidTrunc(e) is strictly supported relative to e'.

Русский

Если K строго поддержан относительно вложения e', то K.stupidTrunc(e) строго поддержан относительно e'.

LaTeX

$$$K\,\.\mathrm{IsStrictlySupported}(e')\Rightarrow (K.\mathrm{stupidTrunc}(e)).\mathrm{IsStrictlySupported}(e')$$$

Lean4

instance {ι'' : Type*} {c'' : ComplexShape ι''} (e' : c''.Embedding c') [K.IsStrictlySupported e'] :
    IsStrictlySupported (K.stupidTrunc e) e' where
  isZero i'
    hi' := by
    by_cases hi'' : ∃ i, e.f i = i'
    · obtain ⟨i, hi⟩ := hi''
      exact (K.isZero_X_of_isStrictlySupported e' i' hi').of_iso (K.stupidTruncXIso e hi)
    · apply isZero_stupidTrunc_X
      simpa using hi''

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