Theorems · Theorem · order theory
SetRel.symm
∀ {α : Type u_1} (R : SetRel α α) {a b : α} [R.IsSymm], (a, b) ∈ R → (b, a) ∈ R- Defined in
- Mathlib.Data.Rel
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- SetRel.IsSymm
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SetRelstatement and proof · cited by 581
- SetRel.IsSymmstatement and proof · cited by 93
- symm_ofproof · cited by 12
Cited by13
Results whose statement or proof uses this declaration.
- comp_symm_of_uniformityproof · cited by 7
- Continuous.uniformContinuous_of_tendsto_cocompactproof · cited by 4
- Equicontinuous.comap_uniformFun_eqproof · cited by 3
- Dynamics.IsDynCoverOf.iterate_le_powproof · cited by 2
- ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOnproof · cited by 2
- IsCompact.uniformContinuousAt_of_continuousAtproof · cited by 1
- equicontinuousWithinAt_iff_pairproof · cited by 1
- Uniform.exists_is_open_mem_uniformity_of_forall_mem_eqproof · cited by 1
- SetRel.isSeparated_insertproof · cited by 1
- UniformSpace.isClosed_ball_of_isSymm_of_isTrans_of_mem_uniformityproof · cited by 1
- Dynamics.IsDynCoverOf.nonempty_interproof · cited by 1
- Dynamics.nonempty_inter_of_coverMincardproof · cited by 0