Theorems · Theorem · general topology

Continuous.matrix_conjTranspose

∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : Star R] [ContinuousStar R] {A : X → Matrix m n R}, Continuous A → Continuous fun x => (A x).conjTranspose

Defined in

Mathlib.Topology.Instances.Matrix

Cited by

3 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceStarContinuousStar