isSupportedOutside_op_iff — Mathlib

English

For K and embedding e, K.op.IsStrictlySupportedOutside e.op iff K.IsStrictlySupportedOutside e.

Русский

Для K и вложения e, K.op.IsStrictlySupportedOutside e.op эквивалентно K.IsStrictlySupportedOutside e.

LaTeX

$$$$ K.op.IsStrictlySupportedOutside e.op \iff K.IsStrictlySupportedOutside e $$$$

Lean4

@[simp]
theorem isSupportedOutside_op_iff : K.op.IsSupportedOutside e.op ↔ K.IsSupportedOutside e :=
  ⟨fun h ↦ ⟨fun i ↦ (h.exactAt i).unop⟩, fun h ↦ ⟨fun i ↦ (h.exactAt i).op⟩⟩

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