isSupported_op_iff — Mathlib

English

For K and embedding e, K.op is supported outside e.op iff K is supported outside e.

Русский

Для K и вложения e, K.op поддержан вне e.op тогда и только тогда, когда K поддержан вне e.

LaTeX

$$$$ K.op.IsSupportedOutside e.op \iff K.IsSupportedOutside e $$$$

Lean4

@[simp]
theorem isSupported_op_iff : K.op.IsSupported e.op ↔ K.IsSupported e :=
  ⟨fun _ ↦ ⟨fun i' hi' ↦ (K.op.exactAt_of_isSupported e.op i' hi').unop⟩, fun _ ↦
    ⟨fun i' hi' ↦ (K.exactAt_of_isSupported e i' hi').op⟩⟩

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