Theorems · Theorem · general topology
isClosed_setOfPred_blockTriangular
∀ {m : Type u_4} {R : Type u_8} [inst : TopologicalSpace R] {α : Type u_11} {b : m → α} [inst_1 : LinearOrder α]
[inst_2 : Zero R] [T2Space R], IsClosed {M | M.BlockTriangular b}- Defined in
- Mathlib.Topology.Instances.Matrix
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- LinearOrderstatement and proof · cited by 8,572
- Set.ofPredstatement · cited by 6,101
- Matrixstatement and proof · cited by 4,303
- IsClosedstatement and proof · cited by 1,639
- T2Spacestatement and proof · cited by 1,351
- Set.iInterproof · cited by 1,084
- continuous_constproof · cited by 278
- continuous_idproof · cited by 192
- isClosed_eqproof · cited by 71
- Set.ofPred_forallproof · cited by 48
- Matrix.BlockTriangularstatement · cited by 45
Cited by2
Results whose statement or proof uses this declaration.
- isClosed_setOf_blockTriangularproof · cited by 0
- Matrix.BlockTriangular.expproof · cited by 0