Invariants

📁 Source: Mathlib/MeasureTheory/MeasurableSpace/Invariants.lean

Statistics

Metric	Count
Definitions invariants	1
Theorems comp_eq_of_measurable_invariants, inf_le_invariants_comp, invariants_id, invariants_le, le_invariants_iterate, measurableSet_invariants, measurable_invariants_dom, measurable_invariants_of_semiconj	8
Total	9

MeasurableSpace

Definitions

Name	Category	Theorems
invariants 📖	CompOp	7 math math: measurable_invariants_dom, invariants_id, invariants_le, measurableSet_invariants, inf_le_invariants_comp, le_invariants_iterate, measurable_invariants_of_semiconj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_eq_of_measurable_invariants 📖	—	Measurable invariants	—	—	MeasurableSingletonClass.measurableSet_singleton Set.mem_preimage Set.mem_singleton_iff
inf_le_invariants_comp 📖	mathematical	—	MeasurableSpace instLE SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice invariants	—	Set.preimage_comp
invariants_id 📖	mathematical	—	invariants	—	ext
invariants_le 📖	mathematical	—	MeasurableSpace instLE invariants	—	—
le_invariants_iterate 📖	mathematical	—	MeasurableSpace instLE invariants Nat.iterate	—	invariants_id le_trans le_inf le_rfl inf_le_invariants_comp
measurableSet_invariants 📖	mathematical	—	MeasurableSet invariants Set.preimage	—	—
measurable_invariants_dom 📖	mathematical	—	Measurable invariants Set.preimage	—	—
measurable_invariants_of_semiconj 📖	mathematical	Measurable Function.Semiconj	invariants	—	Set.preimage_comp Function.Semiconj.comp_eq

---

← Back to Index