## Code Screenshot: Lean 4 Theorem Proofs
### Overview
The image is a screenshot of a code editor window (dark theme) displaying three mathematical theorem statements and their proofs written in the Lean 4 programming language, a dependently typed functional programming language and proof assistant. The content is purely textual code; there are no charts, diagrams, or data visualizations. The text is presented with syntax highlighting.
### Components/Axes
The image contains a single component: a code editor window.
- **Window Controls**: Three colored circles (red, yellow, green) are positioned in the top-left corner, typical of a macOS window interface.
- **Code Content**: The main body contains three distinct theorem blocks. The text is monospaced and uses syntax highlighting:
- Keywords like `theorem`, `by` are in a salmon/pink color.
- Type names like `MeasurableSpace`, `Measure`, `ENNReal` are in a light blue/cyan.
- Identifiers and variables are in a light gray/white.
- Operators (`=`, `:=`, `:`, `<;>`) and punctuation are in white or light gray.
- **Background**: The editor has a dark gray background (`#2d2d2d` approximate). The window itself is centered on a lighter gray background.
### Detailed Analysis / Content Details
The following is a precise transcription of the textual content in the image. The language is **Lean 4**.
**Theorem 1: `ite_pull_measureOf`**
```lean
theorem ite_pull_measureOf {X} [MeasurableSpace X] (c : Prop) [Decidable c]
(μ ν : Measure X) (A : Set X) :
(if c then μ else ν) A
=
(if c then μ A else ν A) := by
split_ifs <;> rfl
```
* **Statement**: For a type `X` with a `MeasurableSpace`, a decidable proposition `c`, two measures `μ` and `ν` on `X`, and a set `A` in `X`, the measure of `A` under the conditionally chosen measure (`μ` if `c` is true, `ν` otherwise) is equal to the conditionally chosen value of the measure of `A` (`μ A` if `c` is true, `ν A` otherwise).
* **Proof**: The proof uses the tactic `split_ifs` to split the goal based on the condition `c`, followed by `rfl` (reflexivity) to close each subgoal.
**Theorem 2: `Measure.prod_volume`**
```lean
theorem Measure.prod_volume {X Y} [MeasureSpace X] [MeasureSpace Y] :
(Measure.prod (volume : Measure X) (volume : Measure Y)) = volume := by
rfl
```
* **Statement**: For types `X` and `Y` each with a `MeasureSpace`, the product measure of the `volume` measure on `X` and the `volume` measure on `Y` is equal to the `volume` measure (on the product space `X × Y`).
* **Proof**: The proof is by reflexivity (`rfl`), indicating this is likely a definitional equality or a previously established lemma.
**Theorem 3: `ite_pull_ennreal_toReal`**
```lean
theorem ite_pull_ennreal_toReal (c : Prop) [Decidable c] (x y : ENNReal) :
(if c then x else y).toReal
=
(if c then x.toReal else y.toReal) := by
split_ifs <;> rfl
```
* **Statement**: For a decidable proposition `c` and two extended non-negative real numbers (`ENNReal`) `x` and `y`, converting the conditionally chosen number (`x` if `c` is true, `y` otherwise) to a real number (`toReal`) is equal to the conditionally chosen conversion (`x.toReal` if `c` is true, `y.toReal` otherwise).
* **Proof**: Identical in structure to the first theorem: `split_ifs <;> rfl`.
### Key Observations
1. **Pattern**: Theorems 1 and 3 share an identical logical structure and proof tactic (`split_ifs <;> rfl`). They both "pull" an operation (`_A` for a measure, `.toReal`) out of a conditional (`if c then ... else ...`).
2. **Context**: The code is from the domain of **measure theory** and **formal verification**. It deals with concepts like measurable spaces, measures, product measures, and extended non-negative reals (`ENNReal`).
3. **Proof Style**: The proofs are extremely concise, relying on basic tactics (`rfl`, `split_ifs`), suggesting these are foundational or definitional lemmas within a larger library (likely Mathlib for Lean).
4. **Visual Layout**: The code is neatly formatted with consistent indentation. The theorems are separated by blank lines for clarity.
### Interpretation
This image does not present data for interpretation in the statistical sense. Instead, it presents **formal mathematical statements** within a proof assistant.
* **What it demonstrates**: The theorems establish basic, likely useful, properties for manipulating conditionals and measures/numbers in a formal setting. They ensure that applying an operation (like evaluating a measure on a set or converting an `ENNReal` to a `Real`) commutes with a conditional choice. This is crucial for simplifying proofs and definitions in formalized mathematics.
* **Relationship between elements**: The three theorems are independent but thematically related. The first and third are direct analogs of each other in different mathematical domains (measure theory vs. real analysis). The second theorem is a separate, fundamental property about product measures.
* **Significance**: In the context of formal verification (proving mathematical theorems with computer assistance), such lemmas are the essential "building blocks." They allow mathematicians and computer scientists to manipulate complex expressions step-by-step in a way that is guaranteed to be logically sound. The image captures a snippet of this meticulous, foundational work.
