Represents

📁 Source: Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean

Statistics

Metric	Count
Definitions Represents, Represents	2
Theorems disjoint_supp_of_notMem, existsUnique_rep, exists_inter_eq_singleton, image_out, ncard_eq, ncard_inter, ncard_sdiff_of_mem, ncard_sdiff_of_notMem, even_ncard_supp_sdiff_rep	9
Total	11

Matrix

Definitions

Name	Category	Theorems
Represents 📖	MathDef	6 math math: isRepresentation.toEnd_represents, Represents.zero, represents_iff, Represents.one, represents_iff', Represents.algebraMap

SimpleGraph.ConnectedComponent

Definitions

Name	Category	Theorems
Represents 📖	MathDef	1 math math: Represents.image_out

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
even_ncard_supp_sdiff_rep 📖	mathematical	Represents SimpleGraph.oddComponents	Even Set.ncard Set Set.instSDiff supp	—	Represents.ncard_sdiff_of_notMem Nat.ne_of_odd_add Nat.not_even_iff_odd Represents.ncard_sdiff_of_mem Nat.even_sub

SimpleGraph.ConnectedComponent.Represents

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_supp_of_notMem 📖	mathematical	SimpleGraph.ConnectedComponent.Represents SimpleGraph.ConnectedComponent Set Set.instMembership	Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SimpleGraph.ConnectedComponent.supp	—	Set.disjoint_left
existsUnique_rep 📖	mathematical	SimpleGraph.ConnectedComponent.Represents SimpleGraph.ConnectedComponent Set Set.instMembership	ExistsUnique Set.instInter SimpleGraph.ConnectedComponent.supp	—	—
exists_inter_eq_singleton 📖	mathematical	SimpleGraph.ConnectedComponent.Represents SimpleGraph.ConnectedComponent Set Set.instMembership	Set.instInter SimpleGraph.ConnectedComponent.supp Set.instSingletonSet	—	existsUnique_rep Set.ext SimpleGraph.Reachable.refl
image_out 📖	mathematical	—	SimpleGraph.ConnectedComponent.Represents Set.image SimpleGraph.Reachable Quot.out	—	Quot.out_eq Set.image_congr
ncard_eq 📖	mathematical	SimpleGraph.ConnectedComponent.Represents	Set.ncard SimpleGraph.ConnectedComponent	—	Set.InjOn.ncard_image Set.BijOn.injOn Set.BijOn.image_eq
ncard_inter 📖	mathematical	SimpleGraph.ConnectedComponent.Represents SimpleGraph.ConnectedComponent Set Set.instMembership	Set.ncard Set.instInter SimpleGraph.ConnectedComponent.supp	—	Set.ncard_eq_one exists_inter_eq_singleton
ncard_sdiff_of_mem 📖	mathematical	SimpleGraph.ConnectedComponent.Represents SimpleGraph.ConnectedComponent Set Set.instMembership	Set.ncard Set.instSDiff SimpleGraph.ConnectedComponent.supp	—	exists_inter_eq_singleton Set.diff_inter_self_eq_diff Set.ncard_diff Set.toFinite Finite.of_fintype Set.ncard_singleton
ncard_sdiff_of_notMem 📖	mathematical	SimpleGraph.ConnectedComponent.Represents SimpleGraph.ConnectedComponent Set Set.instMembership	Set.ncard Set.instSDiff SimpleGraph.ConnectedComponent.supp	—	Disjoint.sdiff_eq_right disjoint_supp_of_notMem

---

← Back to Index